%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT367+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:39 AM UTC 2026
% Result : Theorem 154.11s 41.85s
% Output : Refutation 154.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 73
% Syntax : Number of formulae : 438 ( 82 unt; 51 def)
% Number of atoms : 2641 ( 47 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 3758 (1555 ~;1743 |; 337 &)
% ( 61 <=>; 62 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 85 ( 83 usr; 51 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-4 aty)
% Number of variables : 343 ( 0 sgn 333 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ( v3_waybel_3(k2_yellow_2(X0,X0,X1))
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1)))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1)))
=> ( ( X4 = X2
& X5 = X3 )
=> ( r1_waybel_3(X0,X2,X3)
<=> r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) ) ) ) ) ) ) )
=> v22_waybel_0(X1,X0,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t38_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ( v3_waybel_3(k2_yellow_2(X0,X0,X1))
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1)))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1)))
=> ( ( X4 = X2
& X5 = X3 )
=> ( r1_waybel_3(X0,X2,X3)
<=> r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) ) ) ) ) ) ) )
=> v22_waybel_0(X1,X0,X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f36,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f44,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0) )
=> ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_partfun1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc4_waybel_1) ).
fof(f50,axiom,
! [X0] :
( ( v2_orders_2(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
=> ( v2_orders_2(X1)
& v4_yellow_0(X1,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc6_yellow_0) ).
fof(f52,axiom,
! [X0] :
( ( v3_orders_2(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
=> ( v3_orders_2(X1)
& v4_yellow_0(X1,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc7_yellow_0) ).
fof(f54,axiom,
! [X0] :
( ( v4_orders_2(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
=> ( v4_orders_2(X1)
& v4_yellow_0(X1,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc8_yellow_0) ).
fof(f59,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_orders_2(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_waybel34(X2,X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> ( r1_waybel_3(X0,X3,X4)
=> r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_waybel34) ).
fof(f65,axiom,
! [X0,X1,X2] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& l1_orders_2(X0)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_waybel34) ).
fof(f66,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(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)) )
=> ( v1_funct_1(k2_waybel_1(X0,X1,X2))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_waybel_1) ).
fof(f67,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(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)) )
=> ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_yellow_2) ).
fof(f69,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(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)) )
=> ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_waybel_1) ).
fof(f71,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& ~ v3_struct_0(X1)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,u1_struct_0(X1))
& m1_relset_1(X2,X0,u1_struct_0(X1))
& m1_subset_1(X3,X0) )
=> m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_yellow_2) ).
fof(f73,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f77,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> l1_orders_2(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f88,axiom,
! [X0,X1] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc10_waybel34) ).
fof(f92,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f97,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(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)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_yellow_2) ).
fof(f141,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(f144,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
=> v22_waybel_0(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_waybel34) ).
fof(f146,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v18_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_waybel34) ).
fof(f147,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v22_waybel_0(X1,X0,X0)
<=> v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_waybel34) ).
fof(f148,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k2_yellow_2(X0,X1,X2)))
=> k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),X3) = X3 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_waybel_1) ).
fof(f210,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0) )
=> ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) ) ) ) ),
inference(pure_predicate_removal,[],[f44]) ).
fof(f228,plain,
? [X0] :
( ? [X1] :
( ~ v22_waybel_0(X1,X0,X0)
& v3_waybel_3(k2_yellow_2(X0,X0,X1))
& ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( r1_waybel_3(X0,X2,X3)
<=> r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) )
| X2 != X4
| X3 != X5
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1))) )
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1))) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f229,plain,
? [X0] :
( ? [X1] :
( ~ v22_waybel_0(X1,X0,X0)
& v3_waybel_3(k2_yellow_2(X0,X0,X1))
& ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( r1_waybel_3(X0,X2,X3)
<=> r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) )
| X2 != X4
| X3 != X5
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1))) )
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1))) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f228]) ).
fof(f272,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f273,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f272]) ).
fof(f285,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f210]) ).
fof(f286,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f285]) ).
fof(f297,plain,
! [X0] :
( ! [X1] :
( ( v2_orders_2(X1)
& v4_yellow_0(X1,X0) )
| ~ v4_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f298,plain,
! [X0] :
( ! [X1] :
( ( v2_orders_2(X1)
& v4_yellow_0(X1,X0) )
| ~ v4_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f297]) ).
fof(f301,plain,
! [X0] :
( ! [X1] :
( ( v3_orders_2(X1)
& v4_yellow_0(X1,X0) )
| ~ v4_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f52]) ).
fof(f302,plain,
! [X0] :
( ! [X1] :
( ( v3_orders_2(X1)
& v4_yellow_0(X1,X0) )
| ~ v4_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f301]) ).
fof(f305,plain,
! [X0] :
( ! [X1] :
( ( v4_orders_2(X1)
& v4_yellow_0(X1,X0) )
| ~ v4_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f306,plain,
! [X0] :
( ! [X1] :
( ( v4_orders_2(X1)
& v4_yellow_0(X1,X0) )
| ~ v4_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f305]) ).
fof(f315,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_waybel34(X2,X0,X1)
<=> ! [X3] :
( ! [X4] :
( r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4))
| ~ r1_waybel_3(X0,X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f59]) ).
fof(f316,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_waybel34(X2,X0,X1)
<=> ! [X3] :
( ! [X4] :
( r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4))
| ~ r1_waybel_3(X0,X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f315]) ).
fof(f320,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f65]) ).
fof(f321,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(flattening,[],[f320]) ).
fof(f322,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel_1(X0,X1,X2))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f66]) ).
fof(f323,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel_1(X0,X1,X2))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f322]) ).
fof(f324,plain,
! [X0,X1,X2] :
( ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f67]) ).
fof(f325,plain,
! [X0,X1,X2] :
( ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f324]) ).
fof(f326,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f69]) ).
fof(f327,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f326]) ).
fof(f329,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
| v1_xboole_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,u1_struct_0(X1))
| ~ m1_relset_1(X2,X0,u1_struct_0(X1))
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f330,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
| v1_xboole_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,u1_struct_0(X1))
| ~ m1_relset_1(X2,X0,u1_struct_0(X1))
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f329]) ).
fof(f332,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f333,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f77]) ).
fof(f339,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f88]) ).
fof(f340,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(flattening,[],[f339]) ).
fof(f347,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f92]) ).
fof(f348,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f347]) ).
fof(f356,plain,
! [X0,X1,X2] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f97]) ).
fof(f357,plain,
! [X0,X1,X2] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f356]) ).
fof(f416,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v22_waybel_0(X2,X0,X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f144]) ).
fof(f417,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v22_waybel_0(X2,X0,X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f416]) ).
fof(f420,plain,
! [X0] :
( ! [X1] :
( ( v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v18_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f146]) ).
fof(f421,plain,
! [X0] :
( ! [X1] :
( ( v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v18_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f420]) ).
fof(f422,plain,
! [X0] :
( ! [X1] :
( ( v22_waybel_0(X1,X0,X0)
<=> v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f147]) ).
fof(f423,plain,
! [X0] :
( ! [X1] :
( ( v22_waybel_0(X1,X0,X0)
<=> v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f422]) ).
fof(f424,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),X3) = X3
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_2(X0,X1,X2))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f148]) ).
fof(f425,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),X3) = X3
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_2(X0,X1,X2))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f424]) ).
fof(f437,definition,
! [X1,X0] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ sP2(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f438,plain,
! [X0,X1] :
( sP2(X1,X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(definition_folding,[],[f340,f437]) ).
fof(f451,plain,
? [X0] :
( ? [X1] :
( ~ v22_waybel_0(X1,X0,X0)
& v3_waybel_3(k2_yellow_2(X0,X0,X1))
& ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( ( r1_waybel_3(X0,X2,X3)
| ~ r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) )
& ( r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5)
| ~ r1_waybel_3(X0,X2,X3) ) )
| X2 != X4
| X3 != X5
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1))) )
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1))) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(nnf_transformation,[],[f229]) ).
fof(f452,plain,
( ~ v22_waybel_0(sK10,sK9,sK9)
& v3_waybel_3(k2_yellow_2(sK9,sK9,sK10))
& ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( ( r1_waybel_3(sK9,X2,X3)
| ~ r1_waybel_3(k2_yellow_2(sK9,sK9,sK10),X4,X5) )
& ( r1_waybel_3(k2_yellow_2(sK9,sK9,sK10),X4,X5)
| ~ r1_waybel_3(sK9,X2,X3) ) )
| X2 != X4
| X3 != X5
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_2(sK9,sK9,sK10))) )
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_2(sK9,sK9,sK10))) )
| ~ m1_subset_1(X3,u1_struct_0(sK9)) )
| ~ m1_subset_1(X2,u1_struct_0(sK9)) )
& v1_funct_1(sK10)
& v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
& v8_waybel_1(sK10,sK9)
& m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
& v2_orders_2(sK9)
& v3_orders_2(sK9)
& v4_orders_2(sK9)
& v1_lattice3(sK9)
& v2_lattice3(sK9)
& v3_lattice3(sK9)
& l1_orders_2(sK9) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X0,sK9),skolemize(X1,sK10)],[f451]) ).
fof(f455,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_waybel34(X2,X0,X1)
| ? [X3] :
( ? [X4] :
( ~ r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4))
& r1_waybel_3(X0,X3,X4)
& m1_subset_1(X4,u1_struct_0(X0)) )
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X3] :
( ! [X4] :
( r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4))
| ~ r1_waybel_3(X0,X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v1_waybel34(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f316]) ).
fof(f456,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_waybel34(X2,X0,X1)
| ? [X3] :
( ? [X4] :
( ~ r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4))
& r1_waybel_3(X0,X3,X4)
& m1_subset_1(X4,u1_struct_0(X0)) )
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X5] :
( ! [X6] :
( r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k7_yellow_2(u1_struct_0(X0),X1,X2,X6))
| ~ r1_waybel_3(X0,X5,X6)
| ~ m1_subset_1(X6,u1_struct_0(X0)) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ v1_waybel34(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f455]) ).
fof(f457,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_waybel34(X2,X0,X1)
| ( ~ r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,sK11(X0,X1,X2)),k7_yellow_2(u1_struct_0(X0),X1,X2,sK12(X0,X1,X2)))
& r1_waybel_3(X0,sK11(X0,X1,X2),sK12(X0,X1,X2))
& m1_subset_1(sK12(X0,X1,X2),u1_struct_0(X0))
& m1_subset_1(sK11(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ! [X5] :
( ! [X6] :
( r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k7_yellow_2(u1_struct_0(X0),X1,X2,X6))
| ~ r1_waybel_3(X0,X5,X6)
| ~ m1_subset_1(X6,u1_struct_0(X0)) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ v1_waybel34(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X0,X1,X2)),skolemize(X4,sK12(X0,X1,X2))],[f456]) ).
fof(f464,plain,
! [X1,X0] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ sP2(X1,X0) ),
inference(nnf_transformation,[],[f437]) ).
fof(f465,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X1,X1,X0))
& v1_orders_2(k2_yellow_2(X1,X1,X0))
& v2_orders_2(k2_yellow_2(X1,X1,X0))
& v3_orders_2(k2_yellow_2(X1,X1,X0))
& v4_orders_2(k2_yellow_2(X1,X1,X0))
& v1_yellow_0(k2_yellow_2(X1,X1,X0))
& v2_yellow_0(k2_yellow_2(X1,X1,X0))
& v3_yellow_0(k2_yellow_2(X1,X1,X0))
& v4_yellow_0(k2_yellow_2(X1,X1,X0),X1)
& v24_waybel_0(k2_yellow_2(X1,X1,X0))
& v25_waybel_0(k2_yellow_2(X1,X1,X0))
& v1_lattice3(k2_yellow_2(X1,X1,X0))
& v2_lattice3(k2_yellow_2(X1,X1,X0))
& v3_lattice3(k2_yellow_2(X1,X1,X0)) )
| ~ sP2(X0,X1) ),
inference(rectify,[],[f464]) ).
fof(f499,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,[],[f141]) ).
fof(f500,plain,
! [X0] :
( ! [X1] :
( ( ( v22_waybel_0(X1,X0,X0)
| ~ v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) )
& ( v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
| ~ v22_waybel_0(X1,X0,X0) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f423]) ).
fof(f501,plain,
l1_orders_2(sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f502,plain,
v3_lattice3(sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f503,plain,
v2_lattice3(sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f504,plain,
v1_lattice3(sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f505,plain,
v4_orders_2(sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f506,plain,
v3_orders_2(sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f507,plain,
v2_orders_2(sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f508,plain,
m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9)),
inference(cnf_transformation,[],[f452]) ).
fof(f509,plain,
v8_waybel_1(sK10,sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f510,plain,
v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9)),
inference(cnf_transformation,[],[f452]) ).
fof(f511,plain,
v1_funct_1(sK10),
inference(cnf_transformation,[],[f452]) ).
fof(f513,plain,
! [X2,X3,X4,X5] :
( r1_waybel_3(sK9,X2,X3)
| ~ r1_waybel_3(k2_yellow_2(sK9,sK9,sK10),X4,X5)
| X2 != X4
| X3 != X5
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(X3,u1_struct_0(sK9))
| ~ m1_subset_1(X2,u1_struct_0(sK9)) ),
inference(cnf_transformation,[],[f452]) ).
fof(f514,plain,
v3_waybel_3(k2_yellow_2(sK9,sK9,sK10)),
inference(cnf_transformation,[],[f452]) ).
fof(f515,plain,
~ v22_waybel_0(sK10,sK9,sK9),
inference(cnf_transformation,[],[f452]) ).
fof(f611,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f627,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| v6_waybel_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f286]) ).
fof(f649,plain,
! [X0,X1] :
( ~ v4_yellow_0(X1,X0)
| v2_orders_2(X1)
| ~ m1_yellow_0(X1,X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f298]) ).
fof(f654,plain,
! [X0,X1] :
( ~ v4_yellow_0(X1,X0)
| v3_orders_2(X1)
| ~ m1_yellow_0(X1,X0)
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f302]) ).
fof(f659,plain,
! [X0,X1] :
( ~ v4_yellow_0(X1,X0)
| v4_orders_2(X1)
| ~ m1_yellow_0(X1,X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f306]) ).
fof(f668,plain,
! [X2,X0,X1] :
( m1_subset_1(sK11(X0,X1,X2),u1_struct_0(X0))
| v1_waybel34(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f457]) ).
fof(f669,plain,
! [X2,X0,X1] :
( m1_subset_1(sK12(X0,X1,X2),u1_struct_0(X0))
| v1_waybel34(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f457]) ).
fof(f670,plain,
! [X2,X0,X1] :
( r1_waybel_3(X0,sK11(X0,X1,X2),sK12(X0,X1,X2))
| v1_waybel34(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f457]) ).
fof(f671,plain,
! [X2,X0,X1] :
( ~ r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,sK11(X0,X1,X2)),k7_yellow_2(u1_struct_0(X0),X1,X2,sK12(X0,X1,X2)))
| v1_waybel34(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f457]) ).
fof(f678,plain,
! [X2,X0,X1] :
( v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f321]) ).
fof(f680,plain,
! [X2,X0,X1] :
( m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f323]) ).
fof(f682,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_1(k2_waybel_1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f323]) ).
fof(f683,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f325]) ).
fof(f684,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f325]) ).
fof(f686,plain,
! [X2,X0,X1] :
( m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f327]) ).
fof(f687,plain,
! [X2,X0,X1] :
( v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f327]) ).
fof(f688,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_1(k3_waybel_1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f327]) ).
fof(f692,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
| v1_xboole_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,u1_struct_0(X1))
| ~ m1_relset_1(X2,X0,u1_struct_0(X1))
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f330]) ).
fof(f694,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f332]) ).
fof(f695,plain,
! [X0,X1] :
( ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f333]) ).
fof(f712,plain,
! [X0,X1] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f465]) ).
fof(f713,plain,
! [X0,X1] :
( v2_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f465]) ).
fof(f714,plain,
! [X0,X1] :
( v1_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f465]) ).
fof(f726,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| sP2(X1,X0) ),
inference(cnf_transformation,[],[f438]) ).
fof(f742,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f348]) ).
fof(f770,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_struct_0(k2_yellow_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f357]) ).
fof(f1027,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f499]) ).
fof(f1028,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f499]) ).
fof(f1031,plain,
! [X2,X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| v22_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f417]) ).
fof(f1033,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| k2_waybel_1(X0,X0,X1) = k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f421]) ).
fof(f1034,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| k3_waybel_1(X0,X0,X1) = k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f421]) ).
fof(f1036,plain,
! [X0,X1] :
( v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f421]) ).
fof(f1038,plain,
! [X0,X1] :
( ~ v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
| v22_waybel_0(X1,X0,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f500]) ).
fof(f1039,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k2_yellow_2(X0,X1,X2)))
| k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),X3) = X3
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f425]) ).
fof(f1046,plain,
! [X3,X4,X5] :
( r1_waybel_3(sK9,X4,X3)
| ~ r1_waybel_3(k2_yellow_2(sK9,sK9,sK10),X4,X5)
| X3 != X5
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(X3,u1_struct_0(sK9))
| ~ m1_subset_1(X4,u1_struct_0(sK9)) ),
inference(equality_resolution,[],[f513]) ).
fof(f1047,plain,
! [X4,X5] :
( ~ r1_waybel_3(k2_yellow_2(sK9,sK9,sK10),X4,X5)
| r1_waybel_3(sK9,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(X5,u1_struct_0(sK9))
| ~ m1_subset_1(X4,u1_struct_0(sK9)) ),
inference(equality_resolution,[],[f1046]) ).
fof(f1073,plain,
l1_struct_0(sK9),
inference(resolution,[],[f694,f501]) ).
fof(f1262,definition,
( spl44_17
<=> v3_lattice3(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_17])],[avatar_definition]) ).
fof(f1264,plain,
( ~ v3_lattice3(sK9)
| spl44_17 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1266,definition,
( spl44_18
<=> v3_struct_0(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_18])],[avatar_definition]) ).
fof(f1268,plain,
( v3_struct_0(sK9)
| ~ spl44_18 ),
inference(avatar_component_clause,[],[f1266]) ).
fof(f1276,plain,
( $false
| spl44_17 ),
inference(resolution,[],[f1264,f502]) ).
fof(f1277,plain,
spl44_17,
inference(avatar_contradiction_clause,[],[f1276]) ).
fof(f1284,definition,
( spl44_19
<=> l1_orders_2(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_19])],[avatar_definition]) ).
fof(f1286,plain,
( ~ l1_orders_2(sK9)
| spl44_19 ),
inference(avatar_component_clause,[],[f1284]) ).
fof(f1375,definition,
( spl44_38
<=> v2_orders_2(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_38])],[avatar_definition]) ).
fof(f1377,plain,
( ~ v2_orders_2(sK9)
| spl44_38 ),
inference(avatar_component_clause,[],[f1375]) ).
fof(f1465,plain,
m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9)),
inference(resolution,[],[f1027,f508]) ).
fof(f1474,plain,
( $false
| spl44_38 ),
inference(resolution,[],[f1377,f507]) ).
fof(f1475,plain,
spl44_38,
inference(avatar_contradiction_clause,[],[f1474]) ).
fof(f1476,plain,
( ~ v2_lattice3(sK9)
| ~ l1_orders_2(sK9)
| ~ spl44_18 ),
inference(resolution,[],[f1268,f611]) ).
fof(f1479,definition,
( spl44_53
<=> v1_lattice3(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_53])],[avatar_definition]) ).
fof(f1481,plain,
( ~ v1_lattice3(sK9)
| spl44_53 ),
inference(avatar_component_clause,[],[f1479]) ).
fof(f1484,definition,
( spl44_54
<=> v2_lattice3(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_54])],[avatar_definition]) ).
fof(f1486,plain,
( ~ v2_lattice3(sK9)
| spl44_54 ),
inference(avatar_component_clause,[],[f1484]) ).
fof(f1487,plain,
( ~ spl44_19
| ~ spl44_54
| ~ spl44_18 ),
inference(avatar_split_clause,[],[f1476,f1266,f1484,f1284]) ).
fof(f1494,plain,
( $false
| spl44_19 ),
inference(resolution,[],[f1286,f501]) ).
fof(f1495,plain,
spl44_19,
inference(avatar_contradiction_clause,[],[f1494]) ).
fof(f1566,definition,
( spl44_64
<=> l1_orders_2(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_64])],[avatar_definition]) ).
fof(f1567,plain,
( l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ spl44_64 ),
inference(avatar_component_clause,[],[f1566]) ).
fof(f1574,definition,
( spl44_66
<=> v2_orders_2(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_66])],[avatar_definition]) ).
fof(f1578,definition,
( spl44_67
<=> v3_struct_0(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_67])],[avatar_definition]) ).
fof(f1687,plain,
( $false
| spl44_53 ),
inference(resolution,[],[f1481,f504]) ).
fof(f1688,plain,
spl44_53,
inference(avatar_contradiction_clause,[],[f1687]) ).
fof(f1887,definition,
( spl44_108
<=> v4_orders_2(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_108])],[avatar_definition]) ).
fof(f1889,plain,
( ~ v4_orders_2(sK9)
| spl44_108 ),
inference(avatar_component_clause,[],[f1887]) ).
fof(f1891,definition,
( spl44_109
<=> v3_orders_2(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_109])],[avatar_definition]) ).
fof(f1893,plain,
( ~ v3_orders_2(sK9)
| spl44_109 ),
inference(avatar_component_clause,[],[f1891]) ).
fof(f2209,definition,
( spl44_121
<=> l1_struct_0(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_121])],[avatar_definition]) ).
fof(f2287,definition,
( spl44_124
<=> v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9)) ),
introduced(definition,[new_symbols(definition,[spl44_124])],[avatar_definition]) ).
fof(f2289,plain,
( ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| spl44_124 ),
inference(avatar_component_clause,[],[f2287]) ).
fof(f2291,definition,
( spl44_125
<=> v1_funct_1(sK10) ),
introduced(definition,[new_symbols(definition,[spl44_125])],[avatar_definition]) ).
fof(f2293,plain,
( ~ v1_funct_1(sK10)
| spl44_125 ),
inference(avatar_component_clause,[],[f2291]) ).
fof(f2486,plain,
! [X2,X0,X1] :
( m1_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(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))
| v3_struct_0(X0) ),
inference(resolution,[],[f686,f1027]) ).
fof(f2604,plain,
! [X0,X1] :
( v1_waybel34(X0,k2_yellow_2(sK9,sK9,sK10),X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(X1))
| ~ m2_relset_1(X0,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| r1_waybel_3(sK9,sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(sK9))
| ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(sK9)) ),
inference(resolution,[],[f670,f1047]) ).
fof(f2606,definition,
( spl44_129
<=> ! [X0,X1] :
( v1_waybel34(X0,k2_yellow_2(sK9,sK9,sK10),X1)
| ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(sK9))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(sK9))
| ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| r1_waybel_3(sK9,sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(X1))
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl44_129])],[avatar_definition]) ).
fof(f2607,plain,
( ! [X0,X1] :
( r1_waybel_3(sK9,sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0))
| ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(sK9))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(sK9))
| ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),X1,X0),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| v1_waybel34(X0,k2_yellow_2(sK9,sK9,sK10),X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(X1))
| ~ v1_funct_1(X0) )
| ~ spl44_129 ),
inference(avatar_component_clause,[],[f2606]) ).
fof(f2608,plain,
( ~ spl44_64
| ~ spl44_66
| spl44_67
| spl44_129 ),
inference(avatar_split_clause,[],[f2604,f2606,f1578,f1574,f1566]) ).
fof(f2731,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X3))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v1_waybel34(X4,k2_yellow_2(X0,X1,X2),X3)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X3))
| sK11(k2_yellow_2(X0,X1,X2),X3,X4) = k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),sK11(k2_yellow_2(X0,X1,X2),X3,X4))
| v3_struct_0(X3)
| ~ v2_orders_2(X3)
| ~ l1_orders_2(X3)
| v3_struct_0(k2_yellow_2(X0,X1,X2))
| ~ v2_orders_2(k2_yellow_2(X0,X1,X2))
| ~ l1_orders_2(k2_yellow_2(X0,X1,X2)) ),
inference(resolution,[],[f1039,f668]) ).
fof(f2732,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X3))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v1_waybel34(X4,k2_yellow_2(X0,X1,X2),X3)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X3))
| sK12(k2_yellow_2(X0,X1,X2),X3,X4) = k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),sK12(k2_yellow_2(X0,X1,X2),X3,X4))
| v3_struct_0(X3)
| ~ v2_orders_2(X3)
| ~ l1_orders_2(X3)
| v3_struct_0(k2_yellow_2(X0,X1,X2))
| ~ v2_orders_2(k2_yellow_2(X0,X1,X2))
| ~ l1_orders_2(k2_yellow_2(X0,X1,X2)) ),
inference(resolution,[],[f1039,f669]) ).
fof(f2738,plain,
( ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v8_waybel_1(sK10,sK9)
| k2_waybel_1(sK9,sK9,sK10) = k2_waybel34(sK9,k2_yellow_2(sK9,sK9,sK10),k3_waybel_1(sK9,sK9,sK10))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v1_lattice3(sK9)
| ~ v2_lattice3(sK9)
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9) ),
inference(resolution,[],[f1033,f508]) ).
fof(f2742,definition,
( spl44_130
<=> k2_waybel_1(sK9,sK9,sK10) = k2_waybel34(sK9,k2_yellow_2(sK9,sK9,sK10),k3_waybel_1(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_130])],[avatar_definition]) ).
fof(f2744,plain,
( k2_waybel_1(sK9,sK9,sK10) = k2_waybel34(sK9,k2_yellow_2(sK9,sK9,sK10),k3_waybel_1(sK9,sK9,sK10))
| ~ spl44_130 ),
inference(avatar_component_clause,[],[f2742]) ).
fof(f2746,definition,
( spl44_131
<=> v8_waybel_1(sK10,sK9) ),
introduced(definition,[new_symbols(definition,[spl44_131])],[avatar_definition]) ).
fof(f2748,plain,
( ~ v8_waybel_1(sK10,sK9)
| spl44_131 ),
inference(avatar_component_clause,[],[f2746]) ).
fof(f2749,plain,
( ~ spl44_19
| ~ spl44_17
| ~ spl44_54
| ~ spl44_53
| ~ spl44_108
| ~ spl44_109
| ~ spl44_38
| spl44_130
| ~ spl44_131
| ~ spl44_124
| ~ spl44_125 ),
inference(avatar_split_clause,[],[f2738,f2291,f2287,f2746,f2742,f1375,f1891,f1887,f1479,f1484,f1262,f1284]) ).
fof(f2752,plain,
( ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v8_waybel_1(sK10,sK9)
| k3_waybel_1(sK9,sK9,sK10) = k1_waybel34(sK9,k2_yellow_2(sK9,sK9,sK10),k2_waybel_1(sK9,sK9,sK10))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v1_lattice3(sK9)
| ~ v2_lattice3(sK9)
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9) ),
inference(resolution,[],[f1034,f508]) ).
fof(f2756,definition,
( spl44_132
<=> k3_waybel_1(sK9,sK9,sK10) = k1_waybel34(sK9,k2_yellow_2(sK9,sK9,sK10),k2_waybel_1(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_132])],[avatar_definition]) ).
fof(f2758,plain,
( k3_waybel_1(sK9,sK9,sK10) = k1_waybel34(sK9,k2_yellow_2(sK9,sK9,sK10),k2_waybel_1(sK9,sK9,sK10))
| ~ spl44_132 ),
inference(avatar_component_clause,[],[f2756]) ).
fof(f2759,plain,
( ~ spl44_19
| ~ spl44_17
| ~ spl44_54
| ~ spl44_53
| ~ spl44_108
| ~ spl44_109
| ~ spl44_38
| spl44_132
| ~ spl44_131
| ~ spl44_124
| ~ spl44_125 ),
inference(avatar_split_clause,[],[f2752,f2291,f2287,f2746,f2756,f1375,f1891,f1887,f1479,f1484,f1262,f1284]) ).
fof(f2871,plain,
( $false
| spl44_108 ),
inference(resolution,[],[f1889,f505]) ).
fof(f2872,plain,
spl44_108,
inference(avatar_contradiction_clause,[],[f2871]) ).
fof(f2880,plain,
( $false
| spl44_109 ),
inference(resolution,[],[f1893,f506]) ).
fof(f2881,plain,
spl44_109,
inference(avatar_contradiction_clause,[],[f2880]) ).
fof(f2886,plain,
( ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v8_waybel_1(sK10,sK9)
| v6_waybel_1(sK10,sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9) ),
inference(resolution,[],[f1465,f627]) ).
fof(f2896,plain,
( ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v1_lattice3(sK9)
| ~ v2_lattice3(sK9)
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v6_waybel_1(sK10,sK9)
| sP2(sK10,sK9) ),
inference(resolution,[],[f1465,f726]) ).
fof(f2912,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v1_funct_1(k2_waybel_1(sK9,sK9,sK10)) ),
inference(resolution,[],[f1465,f682]) ).
fof(f2913,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| m1_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9) ),
inference(resolution,[],[f1465,f683]) ).
fof(f2914,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v4_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9) ),
inference(resolution,[],[f1465,f684]) ).
fof(f2916,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v1_funct_1(k3_waybel_1(sK9,sK9,sK10)) ),
inference(resolution,[],[f1465,f688]) ).
fof(f2921,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v3_struct_0(k2_yellow_2(sK9,sK9,sK10)) ),
inference(resolution,[],[f1465,f770]) ).
fof(f2936,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v3_struct_0(k2_yellow_2(sK9,sK9,sK10)) ),
inference(duplicate_literal_removal,[],[f2921]) ).
fof(f2941,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v1_funct_1(k3_waybel_1(sK9,sK9,sK10)) ),
inference(duplicate_literal_removal,[],[f2916]) ).
fof(f2943,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v4_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9) ),
inference(duplicate_literal_removal,[],[f2914]) ).
fof(f2944,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| m1_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9) ),
inference(duplicate_literal_removal,[],[f2913]) ).
fof(f2945,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v1_funct_1(k2_waybel_1(sK9,sK9,sK10)) ),
inference(duplicate_literal_removal,[],[f2912]) ).
fof(f2964,definition,
( spl44_136
<=> l1_struct_0(sK9) ),
introduced(definition,[new_symbols(definition,[spl44_136])],[avatar_definition]) ).
fof(f2966,plain,
( ~ l1_struct_0(sK9)
| spl44_136 ),
inference(avatar_component_clause,[],[f2964]) ).
fof(f3001,plain,
( ~ spl44_67
| ~ spl44_124
| ~ spl44_125
| ~ spl44_19
| spl44_18 ),
inference(avatar_split_clause,[],[f2936,f1266,f1284,f2291,f2287,f1578]) ).
fof(f3027,definition,
( spl44_149
<=> v1_funct_1(k3_waybel_1(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_149])],[avatar_definition]) ).
fof(f3030,plain,
( spl44_149
| ~ spl44_124
| ~ spl44_125
| ~ spl44_19
| spl44_18 ),
inference(avatar_split_clause,[],[f2941,f1266,f1284,f2291,f2287,f3027]) ).
fof(f3037,definition,
( spl44_151
<=> v4_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9) ),
introduced(definition,[new_symbols(definition,[spl44_151])],[avatar_definition]) ).
fof(f3039,plain,
( v4_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ spl44_151 ),
inference(avatar_component_clause,[],[f3037]) ).
fof(f3040,plain,
( spl44_151
| ~ spl44_124
| ~ spl44_125
| ~ spl44_19
| spl44_18 ),
inference(avatar_split_clause,[],[f2943,f1266,f1284,f2291,f2287,f3037]) ).
fof(f3042,definition,
( spl44_152
<=> m1_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9) ),
introduced(definition,[new_symbols(definition,[spl44_152])],[avatar_definition]) ).
fof(f3044,plain,
( m1_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ spl44_152 ),
inference(avatar_component_clause,[],[f3042]) ).
fof(f3045,plain,
( spl44_152
| ~ spl44_124
| ~ spl44_125
| ~ spl44_19
| spl44_18 ),
inference(avatar_split_clause,[],[f2944,f1266,f1284,f2291,f2287,f3042]) ).
fof(f3047,definition,
( spl44_153
<=> v1_funct_1(k2_waybel_1(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_153])],[avatar_definition]) ).
fof(f3050,plain,
( spl44_153
| ~ spl44_124
| ~ spl44_125
| ~ spl44_19
| spl44_18 ),
inference(avatar_split_clause,[],[f2945,f1266,f1284,f2291,f2287,f3047]) ).
fof(f3071,definition,
( spl44_158
<=> v22_waybel_0(sK10,sK9,sK9) ),
introduced(definition,[new_symbols(definition,[spl44_158])],[avatar_definition]) ).
fof(f3073,plain,
( v22_waybel_0(sK10,sK9,sK9)
| ~ spl44_158 ),
inference(avatar_component_clause,[],[f3071]) ).
fof(f3100,definition,
( spl44_163
<=> sP2(sK10,sK9) ),
introduced(definition,[new_symbols(definition,[spl44_163])],[avatar_definition]) ).
fof(f3104,definition,
( spl44_164
<=> v6_waybel_1(sK10,sK9) ),
introduced(definition,[new_symbols(definition,[spl44_164])],[avatar_definition]) ).
fof(f3107,plain,
( spl44_163
| ~ spl44_164
| ~ spl44_124
| ~ spl44_125
| ~ spl44_19
| ~ spl44_17
| ~ spl44_54
| ~ spl44_53
| ~ spl44_108
| ~ spl44_109
| ~ spl44_38 ),
inference(avatar_split_clause,[],[f2896,f1375,f1891,f1887,f1479,f1484,f1262,f1284,f2291,f2287,f3104,f3100]) ).
fof(f3116,definition,
( spl44_166
<=> v3_orders_2(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_166])],[avatar_definition]) ).
fof(f3121,definition,
( spl44_167
<=> v4_orders_2(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_167])],[avatar_definition]) ).
fof(f3137,plain,
( ~ spl44_19
| spl44_18
| spl44_164
| ~ spl44_131
| ~ spl44_124
| ~ spl44_125 ),
inference(avatar_split_clause,[],[f2886,f2291,f2287,f2746,f3104,f1266,f1284]) ).
fof(f3142,plain,
( $false
| spl44_124 ),
inference(resolution,[],[f2289,f510]) ).
fof(f3143,plain,
spl44_124,
inference(avatar_contradiction_clause,[],[f3142]) ).
fof(f3144,plain,
( $false
| spl44_125 ),
inference(resolution,[],[f2293,f511]) ).
fof(f3145,plain,
spl44_125,
inference(avatar_contradiction_clause,[],[f3144]) ).
fof(f3146,plain,
( $false
| spl44_131 ),
inference(resolution,[],[f2748,f509]) ).
fof(f3147,plain,
spl44_131,
inference(avatar_contradiction_clause,[],[f3146]) ).
fof(f3288,plain,
( $false
| spl44_54 ),
inference(resolution,[],[f1486,f503]) ).
fof(f3289,plain,
spl44_54,
inference(avatar_contradiction_clause,[],[f3288]) ).
fof(f3294,plain,
( v1_funct_2(k2_waybel_1(sK9,sK9,sK10),u1_struct_0(sK9),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v1_lattice3(sK9)
| ~ v2_lattice3(sK9)
| ~ l1_orders_2(sK9)
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ v3_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ v4_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ v1_lattice3(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_lattice3(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m1_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ spl44_130 ),
inference(superposition,[],[f678,f2744]) ).
fof(f3302,plain,
( ~ v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| v22_waybel_0(k2_waybel_1(sK9,sK9,sK10),sK9,k2_yellow_2(sK9,sK9,sK10))
| ~ v1_funct_1(k2_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_2(k2_waybel_1(sK9,sK9,sK10),u1_struct_0(sK9),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ v17_waybel_0(k2_waybel_1(sK9,sK9,sK10),sK9,k2_yellow_2(sK9,sK9,sK10))
| ~ m2_relset_1(k2_waybel_1(sK9,sK9,sK10),u1_struct_0(sK9),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ v3_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ v4_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ v1_lattice3(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_lattice3(k2_yellow_2(sK9,sK9,sK10))
| ~ v3_lattice3(k2_yellow_2(sK9,sK9,sK10))
| ~ v3_waybel_3(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v1_lattice3(sK9)
| ~ v2_lattice3(sK9)
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9)
| ~ spl44_132 ),
inference(superposition,[],[f1031,f2758]) ).
fof(f3343,plain,
( $false
| spl44_136 ),
inference(resolution,[],[f2966,f1073]) ).
fof(f3344,plain,
spl44_136,
inference(avatar_contradiction_clause,[],[f3343]) ).
fof(f4926,plain,
( v4_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ m1_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v4_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ spl44_151 ),
inference(resolution,[],[f3039,f659]) ).
fof(f4927,plain,
( v3_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ m1_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v3_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ spl44_151 ),
inference(resolution,[],[f3039,f654]) ).
fof(f4928,plain,
( v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ m1_yellow_0(k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ spl44_151 ),
inference(resolution,[],[f3039,f649]) ).
fof(f4929,plain,
( ~ spl44_19
| ~ spl44_38
| ~ spl44_152
| spl44_66
| ~ spl44_151 ),
inference(avatar_split_clause,[],[f4928,f3037,f1574,f3042,f1375,f1284]) ).
fof(f4930,plain,
( ~ spl44_19
| ~ spl44_109
| ~ spl44_152
| spl44_166
| ~ spl44_151 ),
inference(avatar_split_clause,[],[f4927,f3037,f3116,f3042,f1891,f1284]) ).
fof(f4931,plain,
( ~ spl44_19
| ~ spl44_108
| ~ spl44_152
| spl44_167
| ~ spl44_151 ),
inference(avatar_split_clause,[],[f4926,f3037,f3121,f3042,f1887,f1284]) ).
fof(f5037,plain,
( l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(sK9)
| ~ spl44_152 ),
inference(resolution,[],[f3044,f695]) ).
fof(f5038,plain,
( ~ spl44_19
| spl44_64
| ~ spl44_152 ),
inference(avatar_split_clause,[],[f5037,f3042,f1566,f1284]) ).
fof(f5045,definition,
( spl44_217
<=> m1_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9)) ),
introduced(definition,[new_symbols(definition,[spl44_217])],[avatar_definition]) ).
fof(f5046,plain,
( m1_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ spl44_217 ),
inference(avatar_component_clause,[],[f5045]) ).
fof(f5047,plain,
( ~ m1_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| spl44_217 ),
inference(avatar_component_clause,[],[f5045]) ).
fof(f5049,definition,
( spl44_218
<=> v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9)) ),
introduced(definition,[new_symbols(definition,[spl44_218])],[avatar_definition]) ).
fof(f5050,plain,
( v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ spl44_218 ),
inference(avatar_component_clause,[],[f5049]) ).
fof(f5051,plain,
( ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| spl44_218 ),
inference(avatar_component_clause,[],[f5049]) ).
fof(f5053,definition,
( spl44_219
<=> v2_lattice3(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_219])],[avatar_definition]) ).
fof(f5055,plain,
( ~ v2_lattice3(k2_yellow_2(sK9,sK9,sK10))
| spl44_219 ),
inference(avatar_component_clause,[],[f5053]) ).
fof(f5057,definition,
( spl44_220
<=> v1_lattice3(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_220])],[avatar_definition]) ).
fof(f5059,plain,
( ~ v1_lattice3(k2_yellow_2(sK9,sK9,sK10))
| spl44_220 ),
inference(avatar_component_clause,[],[f5057]) ).
fof(f5061,definition,
( spl44_221
<=> m2_relset_1(k2_waybel_1(sK9,sK9,sK10),u1_struct_0(sK9),u1_struct_0(k2_yellow_2(sK9,sK9,sK10))) ),
introduced(definition,[new_symbols(definition,[spl44_221])],[avatar_definition]) ).
fof(f5062,plain,
( ~ m2_relset_1(k2_waybel_1(sK9,sK9,sK10),u1_struct_0(sK9),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| spl44_221 ),
inference(avatar_component_clause,[],[f5061]) ).
fof(f5066,definition,
( spl44_222
<=> v1_funct_2(k2_waybel_1(sK9,sK9,sK10),u1_struct_0(sK9),u1_struct_0(k2_yellow_2(sK9,sK9,sK10))) ),
introduced(definition,[new_symbols(definition,[spl44_222])],[avatar_definition]) ).
fof(f5069,plain,
( ~ spl44_217
| ~ spl44_218
| ~ spl44_149
| ~ spl44_64
| ~ spl44_219
| ~ spl44_220
| ~ spl44_167
| ~ spl44_166
| ~ spl44_66
| ~ spl44_19
| ~ spl44_54
| ~ spl44_53
| ~ spl44_108
| ~ spl44_109
| ~ spl44_38
| spl44_222
| ~ spl44_130 ),
inference(avatar_split_clause,[],[f3294,f2742,f5066,f1375,f1891,f1887,f1479,f1484,f1284,f1574,f3116,f3121,f5057,f5053,f1566,f3027,f5049,f5045]) ).
fof(f5075,definition,
( spl44_224
<=> v3_lattice3(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_224])],[avatar_definition]) ).
fof(f5077,plain,
( ~ v3_lattice3(k2_yellow_2(sK9,sK9,sK10))
| spl44_224 ),
inference(avatar_component_clause,[],[f5075]) ).
fof(f5094,definition,
( spl44_228
<=> v17_waybel_0(k2_waybel_1(sK9,sK9,sK10),sK9,k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_228])],[avatar_definition]) ).
fof(f5095,plain,
( ~ v17_waybel_0(k2_waybel_1(sK9,sK9,sK10),sK9,k2_yellow_2(sK9,sK9,sK10))
| spl44_228 ),
inference(avatar_component_clause,[],[f5094]) ).
fof(f5099,definition,
( spl44_229
<=> v3_waybel_3(k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_229])],[avatar_definition]) ).
fof(f5101,plain,
( ~ v3_waybel_3(k2_yellow_2(sK9,sK9,sK10))
| spl44_229 ),
inference(avatar_component_clause,[],[f5099]) ).
fof(f5103,definition,
( spl44_230
<=> v22_waybel_0(k2_waybel_1(sK9,sK9,sK10),sK9,k2_yellow_2(sK9,sK9,sK10)) ),
introduced(definition,[new_symbols(definition,[spl44_230])],[avatar_definition]) ).
fof(f5105,plain,
( v22_waybel_0(k2_waybel_1(sK9,sK9,sK10),sK9,k2_yellow_2(sK9,sK9,sK10))
| ~ spl44_230 ),
inference(avatar_component_clause,[],[f5103]) ).
fof(f5107,definition,
( spl44_231
<=> v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9) ),
introduced(definition,[new_symbols(definition,[spl44_231])],[avatar_definition]) ).
fof(f5110,plain,
( ~ spl44_19
| ~ spl44_17
| ~ spl44_54
| ~ spl44_53
| ~ spl44_108
| ~ spl44_109
| ~ spl44_38
| ~ spl44_64
| ~ spl44_229
| ~ spl44_224
| ~ spl44_219
| ~ spl44_220
| ~ spl44_167
| ~ spl44_166
| ~ spl44_66
| ~ spl44_221
| ~ spl44_228
| ~ spl44_222
| ~ spl44_153
| spl44_230
| ~ spl44_231
| ~ spl44_132 ),
inference(avatar_split_clause,[],[f3302,f2756,f5107,f5103,f3047,f5066,f5094,f5061,f1574,f3116,f3121,f5057,f5053,f5075,f5099,f1566,f1375,f1891,f1887,f1479,f1484,f1262,f1284]) ).
fof(f5133,definition,
( spl44_236
<=> m2_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9)) ),
introduced(definition,[new_symbols(definition,[spl44_236])],[avatar_definition]) ).
fof(f5150,plain,
( l1_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ spl44_64 ),
inference(resolution,[],[f1567,f694]) ).
fof(f5167,plain,
( spl44_121
| ~ spl44_64 ),
inference(avatar_split_clause,[],[f5150,f1566,f2209]) ).
fof(f5506,plain,
( ~ sP2(sK10,sK9)
| spl44_220 ),
inference(resolution,[],[f5059,f714]) ).
fof(f5509,plain,
( ~ spl44_163
| spl44_220 ),
inference(avatar_split_clause,[],[f5506,f5057,f3100]) ).
fof(f5537,plain,
( ~ sP2(sK10,sK9)
| spl44_219 ),
inference(resolution,[],[f5055,f713]) ).
fof(f5540,plain,
( ~ spl44_163
| spl44_219 ),
inference(avatar_split_clause,[],[f5537,f5053,f3100]) ).
fof(f5639,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v1_waybel34(k3_waybel_1(X1,X2,X0),k2_yellow_2(X1,X2,X0),X2)
| ~ v1_funct_1(k3_waybel_1(X1,X2,X0))
| ~ v1_funct_2(k3_waybel_1(X1,X2,X0),u1_struct_0(k2_yellow_2(X1,X2,X0)),u1_struct_0(X2))
| sK11(k2_yellow_2(X1,X2,X0),X2,k3_waybel_1(X1,X2,X0)) = k7_yellow_2(u1_struct_0(k2_yellow_2(X1,X2,X0)),X2,k3_waybel_1(X1,X2,X0),sK11(k2_yellow_2(X1,X2,X0),X2,k3_waybel_1(X1,X2,X0)))
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(k2_yellow_2(X1,X2,X0))
| ~ v2_orders_2(k2_yellow_2(X1,X2,X0))
| ~ l1_orders_2(k2_yellow_2(X1,X2,X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(resolution,[],[f2731,f686]) ).
fof(f5664,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k3_waybel_1(X1,X2,X0),u1_struct_0(k2_yellow_2(X1,X2,X0)),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v1_waybel34(k3_waybel_1(X1,X2,X0),k2_yellow_2(X1,X2,X0),X2)
| ~ v1_funct_1(k3_waybel_1(X1,X2,X0))
| ~ v1_funct_1(X0)
| sK11(k2_yellow_2(X1,X2,X0),X2,k3_waybel_1(X1,X2,X0)) = k7_yellow_2(u1_struct_0(k2_yellow_2(X1,X2,X0)),X2,k3_waybel_1(X1,X2,X0),sK11(k2_yellow_2(X1,X2,X0),X2,k3_waybel_1(X1,X2,X0)))
| ~ v2_orders_2(X2)
| v3_struct_0(k2_yellow_2(X1,X2,X0))
| ~ v2_orders_2(k2_yellow_2(X1,X2,X0))
| ~ l1_orders_2(k2_yellow_2(X1,X2,X0))
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(duplicate_literal_removal,[],[f5639]) ).
fof(f5669,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v1_waybel34(k3_waybel_1(X1,X2,X0),k2_yellow_2(X1,X2,X0),X2)
| ~ v1_funct_1(k3_waybel_1(X1,X2,X0))
| ~ v1_funct_2(k3_waybel_1(X1,X2,X0),u1_struct_0(k2_yellow_2(X1,X2,X0)),u1_struct_0(X2))
| sK12(k2_yellow_2(X1,X2,X0),X2,k3_waybel_1(X1,X2,X0)) = k7_yellow_2(u1_struct_0(k2_yellow_2(X1,X2,X0)),X2,k3_waybel_1(X1,X2,X0),sK12(k2_yellow_2(X1,X2,X0),X2,k3_waybel_1(X1,X2,X0)))
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(k2_yellow_2(X1,X2,X0))
| ~ v2_orders_2(k2_yellow_2(X1,X2,X0))
| ~ l1_orders_2(k2_yellow_2(X1,X2,X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(resolution,[],[f2732,f686]) ).
fof(f5694,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k3_waybel_1(X1,X2,X0),u1_struct_0(k2_yellow_2(X1,X2,X0)),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v1_waybel34(k3_waybel_1(X1,X2,X0),k2_yellow_2(X1,X2,X0),X2)
| ~ v1_funct_1(k3_waybel_1(X1,X2,X0))
| ~ v1_funct_1(X0)
| sK12(k2_yellow_2(X1,X2,X0),X2,k3_waybel_1(X1,X2,X0)) = k7_yellow_2(u1_struct_0(k2_yellow_2(X1,X2,X0)),X2,k3_waybel_1(X1,X2,X0),sK12(k2_yellow_2(X1,X2,X0),X2,k3_waybel_1(X1,X2,X0)))
| ~ v2_orders_2(X2)
| v3_struct_0(k2_yellow_2(X1,X2,X0))
| ~ v2_orders_2(k2_yellow_2(X1,X2,X0))
| ~ l1_orders_2(k2_yellow_2(X1,X2,X0))
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(duplicate_literal_removal,[],[f5669]) ).
fof(f5697,plain,
( ~ sP2(sK10,sK9)
| spl44_224 ),
inference(resolution,[],[f5077,f712]) ).
fof(f5700,plain,
( ~ spl44_163
| spl44_224 ),
inference(avatar_split_clause,[],[f5697,f5075,f3100]) ).
fof(f5744,plain,
( ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v3_struct_0(sK9)
| spl44_217 ),
inference(resolution,[],[f5047,f2486]) ).
fof(f5745,plain,
( ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| spl44_217 ),
inference(duplicate_literal_removal,[],[f5744]) ).
fof(f5747,definition,
( spl44_260
<=> m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9)) ),
introduced(definition,[new_symbols(definition,[spl44_260])],[avatar_definition]) ).
fof(f5749,plain,
( ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| spl44_260 ),
inference(avatar_component_clause,[],[f5747]) ).
fof(f5750,plain,
( ~ spl44_260
| ~ spl44_124
| ~ spl44_125
| spl44_18
| ~ spl44_19
| spl44_217 ),
inference(avatar_split_clause,[],[f5745,f5045,f1284,f1266,f2291,f2287,f5747]) ).
fof(f5751,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| spl44_221 ),
inference(resolution,[],[f5062,f680]) ).
fof(f5752,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| spl44_221 ),
inference(duplicate_literal_removal,[],[f5751]) ).
fof(f5753,plain,
( ~ spl44_260
| ~ spl44_124
| ~ spl44_125
| ~ spl44_19
| spl44_18
| spl44_221 ),
inference(avatar_split_clause,[],[f5752,f5061,f1266,f1284,f2291,f2287,f5747]) ).
fof(f5826,definition,
( spl44_267
<=> m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9)) ),
introduced(definition,[new_symbols(definition,[spl44_267])],[avatar_definition]) ).
fof(f5828,plain,
( ~ m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| spl44_267 ),
inference(avatar_component_clause,[],[f5826]) ).
fof(f5919,definition,
( spl44_270
<=> v1_xboole_0(u1_struct_0(k2_yellow_2(sK9,sK9,sK10))) ),
introduced(definition,[new_symbols(definition,[spl44_270])],[avatar_definition]) ).
fof(f5921,plain,
( v1_xboole_0(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ spl44_270 ),
inference(avatar_component_clause,[],[f5919]) ).
fof(f6106,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| spl44_218 ),
inference(resolution,[],[f5051,f687]) ).
fof(f6107,plain,
( v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| spl44_218 ),
inference(duplicate_literal_removal,[],[f6106]) ).
fof(f6108,plain,
( ~ spl44_260
| ~ spl44_124
| ~ spl44_125
| ~ spl44_19
| spl44_18
| spl44_218 ),
inference(avatar_split_clause,[],[f6107,f5049,f1266,f1284,f2291,f2287,f5747]) ).
fof(f6463,plain,
( $false
| spl44_260 ),
inference(resolution,[],[f5749,f1465]) ).
fof(f6464,plain,
spl44_260,
inference(avatar_contradiction_clause,[],[f6463]) ).
fof(f6473,plain,
( ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v8_waybel_1(sK10,sK9)
| ~ m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v1_lattice3(sK9)
| ~ v2_lattice3(sK9)
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9)
| spl44_228 ),
inference(resolution,[],[f5095,f1036]) ).
fof(f6474,plain,
( ~ spl44_19
| ~ spl44_17
| ~ spl44_54
| ~ spl44_53
| ~ spl44_108
| ~ spl44_109
| ~ spl44_38
| ~ spl44_267
| ~ spl44_131
| ~ spl44_124
| ~ spl44_125
| spl44_228 ),
inference(avatar_split_clause,[],[f6473,f5094,f2291,f2287,f2746,f5826,f1375,f1891,f1887,f1479,f1484,f1262,f1284]) ).
fof(f6505,plain,
( m2_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ spl44_217 ),
inference(resolution,[],[f5046,f1028]) ).
fof(f6506,plain,
( spl44_236
| ~ spl44_217 ),
inference(avatar_split_clause,[],[f6505,f5045,f5133]) ).
fof(f6778,definition,
( spl44_387
<=> sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)) = k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10))) ),
introduced(definition,[new_symbols(definition,[spl44_387])],[avatar_definition]) ).
fof(f6780,plain,
( sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)) = k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| ~ spl44_387 ),
inference(avatar_component_clause,[],[f6778]) ).
fof(f6783,definition,
( spl44_388
<=> sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)) = k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10))) ),
introduced(definition,[new_symbols(definition,[spl44_388])],[avatar_definition]) ).
fof(f6785,plain,
( sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)) = k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| ~ spl44_388 ),
inference(avatar_component_clause,[],[f6783]) ).
fof(f7155,plain,
( $false
| spl44_267 ),
inference(resolution,[],[f5828,f508]) ).
fof(f7156,plain,
spl44_267,
inference(avatar_contradiction_clause,[],[f7155]) ).
fof(f7168,plain,
( $false
| spl44_229 ),
inference(resolution,[],[f5101,f514]) ).
fof(f7169,plain,
spl44_229,
inference(avatar_contradiction_clause,[],[f7168]) ).
fof(f7170,plain,
( v22_waybel_0(sK10,sK9,sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v8_waybel_1(sK10,sK9)
| ~ m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v1_lattice3(sK9)
| ~ v2_lattice3(sK9)
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9)
| ~ spl44_230 ),
inference(resolution,[],[f5105,f1038]) ).
fof(f7171,plain,
( ~ spl44_19
| ~ spl44_17
| ~ spl44_54
| ~ spl44_53
| ~ spl44_108
| ~ spl44_109
| ~ spl44_38
| ~ spl44_267
| ~ spl44_131
| ~ spl44_124
| ~ spl44_125
| spl44_158
| ~ spl44_230 ),
inference(avatar_split_clause,[],[f7170,f5103,f3071,f2291,f2287,f2746,f5826,f1375,f1891,f1887,f1479,f1484,f1262,f1284]) ).
fof(f7172,plain,
( $false
| ~ spl44_158 ),
inference(resolution,[],[f3073,f515]) ).
fof(f7173,plain,
~ spl44_158,
inference(avatar_contradiction_clause,[],[f7172]) ).
fof(f7179,plain,
( v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ spl44_270 ),
inference(resolution,[],[f5921,f742]) ).
fof(f7189,plain,
( ~ spl44_121
| spl44_67
| ~ spl44_270 ),
inference(avatar_split_clause,[],[f7179,f5919,f1578,f2209]) ).
fof(f12708,plain,
( ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_1(sK10)
| sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)) = k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| ~ v2_orders_2(sK9)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ spl44_218 ),
inference(resolution,[],[f5664,f5050]) ).
fof(f12709,plain,
( ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_1(sK10)
| sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)) = k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| ~ v2_orders_2(sK9)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ spl44_218 ),
inference(duplicate_literal_removal,[],[f12708]) ).
fof(f12711,plain,
( ~ spl44_260
| ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_38
| spl44_387
| ~ spl44_125
| ~ spl44_149
| spl44_231
| ~ spl44_19
| spl44_18
| ~ spl44_267
| ~ spl44_124
| ~ spl44_218 ),
inference(avatar_split_clause,[],[f12709,f5049,f2287,f5826,f1266,f1284,f5107,f3027,f2291,f6778,f1375,f1578,f1574,f1566,f5747]) ).
fof(f12713,plain,
( ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_1(sK10)
| sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)) = k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| ~ v2_orders_2(sK9)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ spl44_218 ),
inference(resolution,[],[f5694,f5050]) ).
fof(f12714,plain,
( ~ v1_funct_2(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ l1_orders_2(sK9)
| v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_1(sK10)
| sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)) = k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| ~ v2_orders_2(sK9)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ m1_relset_1(sK10,u1_struct_0(sK9),u1_struct_0(sK9))
| ~ spl44_218 ),
inference(duplicate_literal_removal,[],[f12713]) ).
fof(f12716,plain,
( ~ spl44_260
| ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_38
| spl44_388
| ~ spl44_125
| ~ spl44_149
| spl44_231
| ~ spl44_19
| spl44_18
| ~ spl44_267
| ~ spl44_124
| ~ spl44_218 ),
inference(avatar_split_clause,[],[f12714,f5049,f2287,f5826,f1266,f1284,f5107,f3027,f2291,f6783,f1375,f1578,f1574,f1566,f5747]) ).
fof(f15893,plain,
( m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(sK9))
| v1_xboole_0(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| v3_struct_0(sK9)
| ~ l1_struct_0(sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m1_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ spl44_387 ),
inference(superposition,[],[f692,f6780]) ).
fof(f15895,definition,
( spl44_1427
<=> m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(k2_yellow_2(sK9,sK9,sK10))) ),
introduced(definition,[new_symbols(definition,[spl44_1427])],[avatar_definition]) ).
fof(f15897,plain,
( ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| spl44_1427 ),
inference(avatar_component_clause,[],[f15895]) ).
fof(f15899,definition,
( spl44_1428
<=> m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(sK9)) ),
introduced(definition,[new_symbols(definition,[spl44_1428])],[avatar_definition]) ).
fof(f15902,plain,
( ~ spl44_1427
| ~ spl44_217
| ~ spl44_218
| ~ spl44_149
| ~ spl44_136
| spl44_18
| spl44_270
| spl44_1428
| ~ spl44_387 ),
inference(avatar_split_clause,[],[f15893,f6778,f15899,f5919,f1266,f2964,f3027,f5049,f5045,f15895]) ).
fof(f15918,plain,
( ~ r1_waybel_3(sK9,k7_yellow_2(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),sK9,k3_waybel_1(sK9,sK9,sK10),sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10))),sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m2_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ spl44_388 ),
inference(superposition,[],[f671,f6785]) ).
fof(f15923,plain,
( m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(sK9))
| v1_xboole_0(u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| v3_struct_0(sK9)
| ~ l1_struct_0(sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m1_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ spl44_388 ),
inference(superposition,[],[f692,f6785]) ).
fof(f15925,definition,
( spl44_1432
<=> m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(k2_yellow_2(sK9,sK9,sK10))) ),
introduced(definition,[new_symbols(definition,[spl44_1432])],[avatar_definition]) ).
fof(f15927,plain,
( ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| spl44_1432 ),
inference(avatar_component_clause,[],[f15925]) ).
fof(f15929,definition,
( spl44_1433
<=> m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(sK9)) ),
introduced(definition,[new_symbols(definition,[spl44_1433])],[avatar_definition]) ).
fof(f15932,plain,
( ~ spl44_1432
| ~ spl44_217
| ~ spl44_218
| ~ spl44_149
| ~ spl44_136
| spl44_18
| spl44_270
| spl44_1433
| ~ spl44_388 ),
inference(avatar_split_clause,[],[f15923,f6783,f15929,f5919,f1266,f2964,f3027,f5049,f5045,f15925]) ).
fof(f15943,plain,
( ~ r1_waybel_3(sK9,sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m2_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ spl44_387
| ~ spl44_388 ),
inference(forward_demodulation,[],[f15918,f6780]) ).
fof(f15945,definition,
( spl44_1436
<=> r1_waybel_3(sK9,sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10))) ),
introduced(definition,[new_symbols(definition,[spl44_1436])],[avatar_definition]) ).
fof(f15947,plain,
( ~ r1_waybel_3(sK9,sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)))
| spl44_1436 ),
inference(avatar_component_clause,[],[f15945]) ).
fof(f15948,plain,
( ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_19
| ~ spl44_38
| spl44_18
| ~ spl44_236
| ~ spl44_218
| ~ spl44_149
| spl44_231
| ~ spl44_1436
| ~ spl44_387
| ~ spl44_388 ),
inference(avatar_split_clause,[],[f15943,f6783,f6778,f15945,f5107,f3027,f5049,f5133,f1266,f1375,f1284,f1578,f1574,f1566]) ).
fof(f52348,plain,
( v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m2_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| spl44_1427 ),
inference(resolution,[],[f15897,f668]) ).
fof(f52349,plain,
( ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_19
| ~ spl44_38
| spl44_18
| ~ spl44_236
| ~ spl44_218
| ~ spl44_149
| spl44_231
| spl44_1427 ),
inference(avatar_split_clause,[],[f52348,f15895,f5107,f3027,f5049,f5133,f1266,f1375,f1284,f1578,f1574,f1566]) ).
fof(f52498,plain,
( v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m2_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| v3_struct_0(k2_yellow_2(sK9,sK9,sK10))
| ~ v2_orders_2(k2_yellow_2(sK9,sK9,sK10))
| ~ l1_orders_2(k2_yellow_2(sK9,sK9,sK10))
| spl44_1432 ),
inference(resolution,[],[f15927,f669]) ).
fof(f52499,plain,
( ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_19
| ~ spl44_38
| spl44_18
| ~ spl44_236
| ~ spl44_218
| ~ spl44_149
| spl44_231
| spl44_1432 ),
inference(avatar_split_clause,[],[f52498,f15925,f5107,f3027,f5049,f5133,f1266,f1375,f1284,f1578,f1574,f1566]) ).
fof(f56485,plain,
( ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ m1_subset_1(sK11(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| ~ m1_subset_1(sK12(k2_yellow_2(sK9,sK9,sK10),sK9,k3_waybel_1(sK9,sK9,sK10)),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)))
| v1_waybel34(k3_waybel_1(sK9,sK9,sK10),k2_yellow_2(sK9,sK9,sK10),sK9)
| ~ l1_orders_2(sK9)
| ~ v2_orders_2(sK9)
| v3_struct_0(sK9)
| ~ m2_relset_1(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ v1_funct_2(k3_waybel_1(sK9,sK9,sK10),u1_struct_0(k2_yellow_2(sK9,sK9,sK10)),u1_struct_0(sK9))
| ~ v1_funct_1(k3_waybel_1(sK9,sK9,sK10))
| ~ spl44_129
| spl44_1436 ),
inference(resolution,[],[f15947,f2607]) ).
fof(f56486,plain,
( ~ spl44_149
| ~ spl44_218
| ~ spl44_236
| spl44_18
| ~ spl44_38
| ~ spl44_19
| spl44_231
| ~ spl44_1432
| ~ spl44_1427
| ~ spl44_1433
| ~ spl44_1428
| ~ spl44_129
| spl44_1436 ),
inference(avatar_split_clause,[],[f56485,f15945,f2606,f15899,f15929,f15895,f15925,f5107,f1284,f1375,f1266,f5133,f5049,f3027]) ).
cnf(s10,plain,
spl44_17,
inference(sat_conversion,[],[f1277]) ).
cnf(s34,plain,
spl44_38,
inference(sat_conversion,[],[f1475]) ).
cnf(s36,plain,
( ~ spl44_18
| ~ spl44_19
| ~ spl44_54 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s37,plain,
spl44_19,
inference(sat_conversion,[],[f1495]) ).
cnf(s52,plain,
spl44_53,
inference(sat_conversion,[],[f1688]) ).
cnf(s76,plain,
( ~ spl44_64
| ~ spl44_66
| spl44_67
| spl44_129 ),
inference(sat_conversion,[],[f2608]) ).
cnf(s78,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_108
| ~ spl44_109
| ~ spl44_124
| ~ spl44_125
| spl44_130
| ~ spl44_131 ),
inference(sat_conversion,[],[f2749]) ).
cnf(s79,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_108
| ~ spl44_109
| ~ spl44_124
| ~ spl44_125
| ~ spl44_131
| spl44_132 ),
inference(sat_conversion,[],[f2759]) ).
cnf(s81,plain,
spl44_108,
inference(sat_conversion,[],[f2872]) ).
cnf(s83,plain,
spl44_109,
inference(sat_conversion,[],[f2881]) ).
cnf(s90,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_67
| ~ spl44_124
| ~ spl44_125 ),
inference(sat_conversion,[],[f3001]) ).
cnf(s95,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_149 ),
inference(sat_conversion,[],[f3030]) ).
cnf(s97,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_151 ),
inference(sat_conversion,[],[f3040]) ).
cnf(s98,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_152 ),
inference(sat_conversion,[],[f3045]) ).
cnf(s99,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_153 ),
inference(sat_conversion,[],[f3050]) ).
cnf(s112,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_108
| ~ spl44_109
| ~ spl44_124
| ~ spl44_125
| spl44_163
| ~ spl44_164 ),
inference(sat_conversion,[],[f3107]) ).
cnf(s122,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| ~ spl44_131
| spl44_164 ),
inference(sat_conversion,[],[f3137]) ).
cnf(s127,plain,
spl44_124,
inference(sat_conversion,[],[f3143]) ).
cnf(s128,plain,
spl44_125,
inference(sat_conversion,[],[f3145]) ).
cnf(s129,plain,
spl44_131,
inference(sat_conversion,[],[f3147]) ).
cnf(s162,plain,
spl44_54,
inference(sat_conversion,[],[f3289]) ).
cnf(s179,plain,
spl44_136,
inference(sat_conversion,[],[f3344]) ).
cnf(s237,plain,
( ~ spl44_19
| ~ spl44_38
| spl44_66
| ~ spl44_151
| ~ spl44_152 ),
inference(sat_conversion,[],[f4929]) ).
cnf(s238,plain,
( ~ spl44_19
| ~ spl44_109
| ~ spl44_151
| ~ spl44_152
| spl44_166 ),
inference(sat_conversion,[],[f4930]) ).
cnf(s239,plain,
( ~ spl44_19
| ~ spl44_108
| ~ spl44_151
| ~ spl44_152
| spl44_167 ),
inference(sat_conversion,[],[f4931]) ).
cnf(s241,plain,
( ~ spl44_19
| spl44_64
| ~ spl44_152 ),
inference(sat_conversion,[],[f5038]) ).
cnf(s248,plain,
( ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_64
| ~ spl44_66
| ~ spl44_108
| ~ spl44_109
| ~ spl44_130
| ~ spl44_149
| ~ spl44_166
| ~ spl44_167
| ~ spl44_217
| ~ spl44_218
| ~ spl44_219
| ~ spl44_220
| spl44_222 ),
inference(sat_conversion,[],[f5069]) ).
cnf(s253,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_64
| ~ spl44_66
| ~ spl44_108
| ~ spl44_109
| ~ spl44_132
| ~ spl44_153
| ~ spl44_166
| ~ spl44_167
| ~ spl44_219
| ~ spl44_220
| ~ spl44_221
| ~ spl44_222
| ~ spl44_224
| ~ spl44_228
| ~ spl44_229
| spl44_230
| ~ spl44_231 ),
inference(sat_conversion,[],[f5110]) ).
cnf(s265,plain,
( ~ spl44_64
| spl44_121 ),
inference(sat_conversion,[],[f5167]) ).
cnf(s288,plain,
( ~ spl44_163
| spl44_220 ),
inference(sat_conversion,[],[f5509]) ).
cnf(s290,plain,
( ~ spl44_163
| spl44_219 ),
inference(sat_conversion,[],[f5540]) ).
cnf(s297,plain,
( ~ spl44_163
| spl44_224 ),
inference(sat_conversion,[],[f5700]) ).
cnf(s306,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_217
| ~ spl44_260 ),
inference(sat_conversion,[],[f5750]) ).
cnf(s307,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_221
| ~ spl44_260 ),
inference(sat_conversion,[],[f5753]) ).
cnf(s359,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_218
| ~ spl44_260 ),
inference(sat_conversion,[],[f6108]) ).
cnf(s420,plain,
spl44_260,
inference(sat_conversion,[],[f6464]) ).
cnf(s424,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_108
| ~ spl44_109
| ~ spl44_124
| ~ spl44_125
| ~ spl44_131
| spl44_228
| ~ spl44_267 ),
inference(sat_conversion,[],[f6474]) ).
cnf(s425,plain,
( ~ spl44_217
| spl44_236 ),
inference(sat_conversion,[],[f6506]) ).
cnf(s565,plain,
spl44_267,
inference(sat_conversion,[],[f7156]) ).
cnf(s569,plain,
spl44_229,
inference(sat_conversion,[],[f7169]) ).
cnf(s570,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_108
| ~ spl44_109
| ~ spl44_124
| ~ spl44_125
| ~ spl44_131
| spl44_158
| ~ spl44_230
| ~ spl44_267 ),
inference(sat_conversion,[],[f7171]) ).
cnf(s571,plain,
~ spl44_158,
inference(sat_conversion,[],[f7173]) ).
cnf(s574,plain,
( spl44_67
| ~ spl44_121
| ~ spl44_270 ),
inference(sat_conversion,[],[f7189]) ).
cnf(s1251,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_38
| ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_124
| ~ spl44_125
| ~ spl44_149
| ~ spl44_218
| spl44_231
| ~ spl44_260
| ~ spl44_267
| spl44_387 ),
inference(sat_conversion,[],[f12711]) ).
cnf(s1252,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_38
| ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_124
| ~ spl44_125
| ~ spl44_149
| ~ spl44_218
| spl44_231
| ~ spl44_260
| ~ spl44_267
| spl44_388 ),
inference(sat_conversion,[],[f12716]) ).
cnf(s1729,plain,
( spl44_18
| ~ spl44_136
| ~ spl44_149
| ~ spl44_217
| ~ spl44_218
| spl44_270
| ~ spl44_387
| ~ spl44_1427
| spl44_1428 ),
inference(sat_conversion,[],[f15902]) ).
cnf(s1733,plain,
( spl44_18
| ~ spl44_136
| ~ spl44_149
| ~ spl44_217
| ~ spl44_218
| spl44_270
| ~ spl44_388
| ~ spl44_1432
| spl44_1433 ),
inference(sat_conversion,[],[f15932]) ).
cnf(s1736,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_38
| ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_149
| ~ spl44_218
| spl44_231
| ~ spl44_236
| ~ spl44_387
| ~ spl44_388
| ~ spl44_1436 ),
inference(sat_conversion,[],[f15948]) ).
cnf(s7395,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_38
| ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_149
| ~ spl44_218
| spl44_231
| ~ spl44_236
| spl44_1427 ),
inference(sat_conversion,[],[f52349]) ).
cnf(s7425,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_38
| ~ spl44_64
| ~ spl44_66
| spl44_67
| ~ spl44_149
| ~ spl44_218
| spl44_231
| ~ spl44_236
| spl44_1432 ),
inference(sat_conversion,[],[f52499]) ).
cnf(s7944,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_38
| ~ spl44_129
| ~ spl44_149
| ~ spl44_218
| spl44_231
| ~ spl44_236
| ~ spl44_1427
| ~ spl44_1428
| ~ spl44_1432
| ~ spl44_1433
| spl44_1436 ),
inference(sat_conversion,[],[f56486]) ).
cnf(s8045,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_108
| ~ spl44_109
| ~ spl44_124
| ~ spl44_125
| ~ spl44_131
| ~ spl44_230
| ~ spl44_267 ),
inference(rat,[],[s570,s571]) ).
cnf(s8049,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_108
| ~ spl44_109
| ~ spl44_124
| ~ spl44_125
| ~ spl44_131
| spl44_228 ),
inference(rat,[],[s424,s565]) ).
cnf(s8053,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_218 ),
inference(rat,[],[s359,s420]) ).
cnf(s8060,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_221 ),
inference(rat,[],[s307,s420]) ).
cnf(s8061,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_124
| ~ spl44_125
| spl44_217 ),
inference(rat,[],[s306,s420]) ).
cnf(s8062,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_54
| ~ spl44_64
| ~ spl44_66
| ~ spl44_108
| ~ spl44_109
| ~ spl44_132
| ~ spl44_153
| ~ spl44_166
| ~ spl44_167
| ~ spl44_219
| ~ spl44_220
| ~ spl44_221
| ~ spl44_222
| ~ spl44_224
| ~ spl44_228
| spl44_230
| ~ spl44_231 ),
inference(rat,[],[s253,s569]) ).
cnf(s8175,plain,
( spl44_18
| ~ spl44_19
| spl44_164 ),
inference(rat,[],[s122,s129,s128,s127]) ).
cnf(s8185,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| ~ spl44_108
| ~ spl44_109
| spl44_163
| ~ spl44_164 ),
inference(rat,[],[s112,s128,s127,s162]) ).
cnf(s8198,plain,
( spl44_18
| ~ spl44_19
| spl44_153 ),
inference(rat,[],[s99,s128,s127]) ).
cnf(s8199,plain,
( spl44_18
| ~ spl44_19
| spl44_152 ),
inference(rat,[],[s98,s128,s127]) ).
cnf(s8200,plain,
( spl44_18
| ~ spl44_19
| spl44_151 ),
inference(rat,[],[s97,s128,s127]) ).
cnf(s8202,plain,
( spl44_18
| ~ spl44_19
| spl44_149 ),
inference(rat,[],[s95,s128,s127]) ).
cnf(s8207,plain,
( spl44_18
| ~ spl44_19
| ~ spl44_67 ),
inference(rat,[],[s90,s128,s127]) ).
cnf(s8215,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| spl44_132 ),
inference(rat,[],[s79,s129,s128,s127,s83,s81,s162]) ).
cnf(s8216,plain,
( ~ spl44_17
| ~ spl44_19
| ~ spl44_38
| ~ spl44_53
| spl44_130 ),
inference(rat,[],[s78,s129,s128,s127,s83,s81,s162]) ).
cnf(s8271,plain,
~ spl44_18,
inference(rat,[],[s36,s162,s37]) ).
cnf(s8286,plain,
spl44_218,
inference(rat,[],[s8053,s37,s128,s127,s8271]) ).
cnf(s8289,plain,
spl44_221,
inference(rat,[],[s8060,s37,s128,s127,s8271]) ).
cnf(s8290,plain,
spl44_217,
inference(rat,[],[s8061,s37,s128,s127,s8271]) ).
cnf(s8292,plain,
spl44_164,
inference(rat,[],[s8175,s37,s8271]) ).
cnf(s8295,plain,
spl44_153,
inference(rat,[],[s8198,s37,s8271]) ).
cnf(s8296,plain,
spl44_152,
inference(rat,[],[s8199,s37,s8271]) ).
cnf(s8297,plain,
spl44_151,
inference(rat,[],[s8200,s37,s8271]) ).
cnf(s8299,plain,
spl44_149,
inference(rat,[],[s8202,s37,s8271]) ).
cnf(s8300,plain,
~ spl44_67,
inference(rat,[],[s8207,s37,s8271]) ).
cnf(s8335,plain,
spl44_236,
inference(rat,[],[s425,s8290]) ).
cnf(s8338,plain,
spl44_64,
inference(rat,[],[s241,s37,s8296]) ).
cnf(s8339,plain,
spl44_166,
inference(rat,[],[s238,s8296,s37,s83,s8297]) ).
cnf(s8340,plain,
spl44_167,
inference(rat,[],[s239,s8296,s37,s81,s8297]) ).
cnf(s8377,plain,
spl44_121,
inference(rat,[],[s265,s8338]) ).
cnf(s8445,plain,
~ spl44_270,
inference(rat,[],[s574,s8300,s8377]) ).
cnf(s8769,plain,
spl44_66,
inference(rat,[],[s237,s8296,s8297,s37,s34]) ).
cnf(s8838,plain,
spl44_129,
inference(rat,[],[s76,s8338,s8300,s8769]) ).
cnf(s9274,plain,
~ spl44_230,
inference(rat,[],[s8045,s565,s34,s129,s128,s127,s83,s81,s162,s52,s37,s10]) ).
cnf(s9275,plain,
spl44_228,
inference(rat,[],[s8049,s34,s129,s128,s127,s83,s81,s162,s52,s37,s10]) ).
cnf(s9277,plain,
spl44_163,
inference(rat,[],[s8185,s8292,s34,s83,s81,s52,s37,s10]) ).
cnf(s9278,plain,
spl44_132,
inference(rat,[],[s8215,s34,s52,s37,s10]) ).
cnf(s9279,plain,
spl44_130,
inference(rat,[],[s8216,s34,s52,s37,s10]) ).
cnf(s9284,plain,
spl44_224,
inference(rat,[],[s297,s9277]) ).
cnf(s9285,plain,
spl44_219,
inference(rat,[],[s290,s9277]) ).
cnf(s9286,plain,
spl44_220,
inference(rat,[],[s288,s9277]) ).
cnf(s9293,plain,
spl44_222,
inference(rat,[],[s248,s9279,s9286,s8769,s8286,s8290,s8340,s8339,s8299,s34,s83,s81,s8338,s37,s162,s52,s9285]) ).
cnf(s9360,plain,
~ spl44_231,
inference(rat,[],[s8062,s9285,s9274,s9275,s9284,s9278,s8289,s9286,s10,s8340,s8339,s8295,s34,s83,s81,s8769,s8338,s162,s52,s37,s9293]) ).
cnf(s9407,plain,
spl44_1432,
inference(rat,[],[s7425,s8769,s8335,s34,s8286,s8299,s8300,s8338,s8271,s37,s9360]) ).
cnf(s9408,plain,
spl44_1427,
inference(rat,[],[s7395,s8769,s8335,s34,s8286,s8299,s8300,s8338,s8271,s37,s9360]) ).
cnf(s9423,plain,
spl44_388,
inference(rat,[],[s1252,s8769,s565,s420,s34,s8286,s8299,s128,s127,s8300,s8338,s8271,s37,s9360]) ).
cnf(s9424,plain,
spl44_387,
inference(rat,[],[s1251,s8769,s565,s420,s34,s8286,s8299,s128,s127,s8300,s8338,s8271,s37,s9360]) ).
cnf(s9496,plain,
spl44_1433,
inference(rat,[],[s1733,s9407,s8445,s8299,s8290,s8286,s8271,s179,s9423]) ).
cnf(s9500,plain,
spl44_1428,
inference(rat,[],[s1729,s9408,s8445,s8299,s8290,s8286,s8271,s179,s9424]) ).
cnf(s9503,plain,
~ spl44_1436,
inference(rat,[],[s1736,s9423,s9360,s8769,s8335,s34,s8286,s8299,s8300,s8338,s8271,s37,s9424]) ).
cnf(s9617,plain,
$false,
inference(rat,[],[s7944,s9503,s9408,s9407,s9360,s8838,s8335,s34,s8286,s8299,s8271,s37,s9496,s9500]) ).
fof(f56487,plain,
$false,
inference(avatar_sat_refutation,[],[s9617]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT367+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.18/0.44 % Computer : n018.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sun Sep 27 15:07:08 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.22/0.50 Running first-order model finding
% 0.22/0.50 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.31/4.29 % (2472840)Will run a generic schedule for satisfiability detection.
% 26.31/4.29 % (2472850)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1968291963:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 26.31/4.29 % (2472846)% WARNING: option uhcvi not known.
% 26.31/4.29 % (2472846)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3375441283:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 26.31/4.29 % (2472848)dis+10_1_sil=32000:sp=arity:random_seed=3702431054:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 26.31/4.29 % (2472849)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=863798507:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 26.31/4.29 % (2472847)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=881824564:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 26.31/4.29 % (2472845)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4227175651_2999 on theBenchmark for (2999ds/0Mi)
% 26.31/4.29 % (2472851)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2924726087:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 26.31/4.29 % (2472850)Instruction limit reached!
% 26.31/4.29 % (2472850)------------------------------
% 26.31/4.29 % (2472850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.31/4.29 % (2472850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/4.29 % (2472850)CaDiCaL version: 2.1.3
% 26.31/4.29 % (2472850)Termination reason: Instruction limit
% 26.31/4.29 % (2472850)Termination phase: Saturation
% 26.31/4.29 % (2472850)Time elapsed: 0.066 s
% 26.31/4.29 % (2472850)Peak memory usage: 14 MB
% 26.31/4.29 % (2472850)Instructions burned: 131 (million)
% 26.31/4.29 % (2472859)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1465794976:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 26.31/4.29 % TRYING [1]
% 26.31/4.29 % TRYING [2]
% 26.31/4.29 % (2472848)Instruction limit reached!
% 26.31/4.29 % (2472848)------------------------------
% 26.31/4.29 % (2472848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.31/4.29 % (2472848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/4.29 % (2472848)CaDiCaL version: 2.1.3
% 26.31/4.29 % (2472848)Termination reason: Instruction limit
% 26.31/4.29 % (2472848)Termination phase: Saturation
% 26.31/4.29 % (2472848)Time elapsed: 0.098 s
% 26.31/4.29 % (2472848)Peak memory usage: 13 MB
% 26.31/4.29 % (2472848)Instructions burned: 103 (million)
% 26.31/4.29 % (2472849)Instruction limit reached!
% 26.31/4.29 % (2472849)------------------------------
% 26.31/4.29 % (2472849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.31/4.29 % (2472849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/4.29 % (2472849)CaDiCaL version: 2.1.3
% 26.31/4.29 % (2472849)Termination reason: Instruction limit
% 26.31/4.29 % (2472849)Termination phase: Saturation
% 26.31/4.29 % (2472849)Time elapsed: 0.106 s
% 26.31/4.29 % (2472849)Peak memory usage: 13 MB
% 26.31/4.29 % (2472849)Instructions burned: 116 (million)
% 26.31/4.29 % TRYING [1]
% 26.31/4.29 % TRYING [2]
% 26.31/4.29 % (2472861)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2893392947:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 26.31/4.29 % TRYING [3]
% 26.31/4.29 % TRYING [3]
% 26.31/4.29 % (2472862)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=188462128:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 26.31/4.29 % (2472851)Instruction limit reached!
% 26.31/4.29 % (2472851)------------------------------
% 26.31/4.29 % (2472851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.31/4.29 % (2472851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/4.29 % (2472851)CaDiCaL version: 2.1.3
% 26.31/4.29 % (2472851)Termination reason: Instruction limit
% 26.31/4.29 % (2472851)Termination phase: Saturation
% 26.31/4.29 % (2472851)Time elapsed: 0.168 s
% 26.31/4.29 % (2472851)Peak memory usage: 14 MB
% 26.31/4.29 % (2472851)Instructions burned: 159 (million)
% 26.31/4.29 % TRYING [4]
% 26.31/4.29 % (2472865)ott-21_1_sil=16000:fs=off:random_seed=2160824390:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 26.31/4.29 % (2472861)Instruction limit reached!
% 26.31/4.29 % (2472861)------------------------------
% 26.31/4.29 % (2472861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.31/4.29 % (2472861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.69/10.66 % (2472861)CaDiCaL version: 2.1.3
% 71.69/10.66 % (2472861)Termination reason: Instruction limit
% 71.69/10.66 % (2472861)Termination phase: Saturation
% 71.69/10.66 % (2472861)Time elapsed: 0.115 s
% 71.69/10.66 % (2472861)Peak memory usage: 14 MB
% 71.69/10.66 % (2472861)Instructions burned: 132 (million)
% 71.69/10.66 % (2472867)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1476601228:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 71.69/10.66 % TRYING [4]
% 71.69/10.66 % (2472859)Instruction limit reached!
% 71.69/10.66 % (2472859)------------------------------
% 71.69/10.66 % (2472859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.69/10.66 % (2472859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.69/10.66 % (2472859)CaDiCaL version: 2.1.3
% 71.69/10.66 % (2472859)Termination reason: Instruction limit
% 71.69/10.66 % (2472859)Termination phase: Finite model building constraint generation
% 71.69/10.66 % (2472859)Time elapsed: 0.281 s
% 71.69/10.66 % (2472859)Peak memory usage: 36 MB
% 71.69/10.66 % (2472859)Instructions burned: 714 (million)
% 71.69/10.66 % (2472869)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3332790683:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 71.69/10.66 % (2472865)Instruction limit reached!
% 71.69/10.66 % (2472865)------------------------------
% 71.69/10.66 % (2472865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.69/10.66 % (2472865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.69/10.66 % (2472865)CaDiCaL version: 2.1.3
% 71.69/10.66 % (2472865)Termination reason: Instruction limit
% 71.69/10.66 % (2472865)Termination phase: Saturation
% 71.69/10.66 % (2472865)Time elapsed: 0.173 s
% 71.69/10.66 % (2472865)Peak memory usage: 13 MB
% 71.69/10.66 % (2472865)Instructions burned: 180 (million)
% 71.69/10.66 % (2472871)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4101699360:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 71.69/10.66 % TRYING [1]
% 71.69/10.66 % TRYING [2]
% 71.69/10.66 % TRYING [3]
% 71.69/10.66 % (2472869)Instruction limit reached!
% 71.69/10.66 % (2472869)------------------------------
% 71.69/10.66 % (2472869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.69/10.66 % (2472869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.69/10.66 % (2472869)CaDiCaL version: 2.1.3
% 71.69/10.66 % (2472869)Termination reason: Instruction limit
% 71.69/10.66 % (2472869)Termination phase: Finite model building SAT solving
% 71.69/10.66 % (2472869)Time elapsed: 0.336 s
% 71.69/10.66 % (2472869)Peak memory usage: 26 MB
% 71.69/10.66 % (2472869)Instructions burned: 868 (million)
% 71.69/10.66 % (2472873)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3372630361:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 71.69/10.66 % (2472862)Instruction limit reached!
% 71.69/10.66 % (2472862)------------------------------
% 71.69/10.66 % (2472862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.69/10.66 % (2472862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.69/10.66 % (2472862)CaDiCaL version: 2.1.3
% 71.69/10.66 % (2472862)Termination reason: Instruction limit
% 71.69/10.66 % (2472862)Termination phase: Saturation
% 71.69/10.66 % (2472862)Time elapsed: 0.627 s
% 71.69/10.66 % (2472862)Peak memory usage: 21 MB
% 71.69/10.66 % (2472862)Instructions burned: 684 (million)
% 71.69/10.66 % (2472867)Instruction limit reached!
% 71.69/10.66 % (2472867)------------------------------
% 71.69/10.66 % (2472867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.69/10.66 % (2472867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.69/10.66 % (2472867)CaDiCaL version: 2.1.3
% 71.69/10.66 % (2472867)Termination reason: Instruction limit
% 71.69/10.66 % (2472867)Termination phase: Saturation
% 71.69/10.66 % (2472867)Time elapsed: 0.502 s
% 71.69/10.66 % (2472867)Peak memory usage: 16 MB
% 71.69/10.66 % (2472867)Instructions burned: 477 (million)
% 71.69/10.66 % (2472875)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3983737656:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 71.69/10.66 % (2472876)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2086214875:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 71.69/10.66 % TRYING [5]
% 71.69/10.66 % (2472873)Instruction limit reached!
% 71.69/10.66 % (2472873)------------------------------
% 71.69/10.66 % (2472873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.48/17.09 % (2472873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.09 % (2472873)CaDiCaL version: 2.1.3
% 117.48/17.09 % (2472873)Termination reason: Instruction limit
% 117.48/17.09 % (2472873)Termination phase: Finite model building constraint generation
% 117.48/17.09 % (2472873)Time elapsed: 0.446 s
% 117.48/17.09 % (2472873)Peak memory usage: 102 MB
% 117.48/17.09 % (2472873)Instructions burned: 889 (million)
% 117.48/17.09 % (2472879)fmb+10_1_sil=64000:random_seed=3501759888:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 117.48/17.09 % TRYING [1]
% 117.48/17.09 % TRYING [2]
% 117.48/17.09 % TRYING [3]
% 117.48/17.09 % (2472875)Instruction limit reached!
% 117.48/17.09 % (2472875)------------------------------
% 117.48/17.09 % (2472875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.48/17.09 % (2472875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.09 % (2472875)CaDiCaL version: 2.1.3
% 117.48/17.09 % (2472875)Termination reason: Instruction limit
% 117.48/17.09 % (2472875)Termination phase: Saturation
% 117.48/17.09 % (2472875)Time elapsed: 0.674 s
% 117.48/17.09 % (2472875)Peak memory usage: 22 MB
% 117.48/17.09 % (2472875)Instructions burned: 693 (million)
% 117.48/17.09 % (2472871)Instruction limit reached!
% 117.48/17.09 % (2472871)------------------------------
% 117.48/17.09 % (2472871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.48/17.09 % (2472871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.09 % (2472871)CaDiCaL version: 2.1.3
% 117.48/17.09 % (2472871)Termination reason: Instruction limit
% 117.48/17.09 % (2472871)Termination phase: Saturation
% 117.48/17.09 % (2472871)Time elapsed: 1.088 s
% 117.48/17.09 % (2472871)Peak memory usage: 26 MB
% 117.48/17.09 % (2472871)Instructions burned: 1179 (million)
% 117.48/17.09 % TRYING [4]
% 117.48/17.09 % (2472881)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=642035120:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 117.48/17.09 % (2472882)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1311988540:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 117.48/17.09 % TRYING [20]
% 117.48/17.09 % (2472876)Instruction limit reached!
% 117.48/17.09 % (2472876)------------------------------
% 117.48/17.09 % (2472876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.48/17.09 % (2472876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.09 % (2472876)CaDiCaL version: 2.1.3
% 117.48/17.09 % (2472876)Termination reason: Instruction limit
% 117.48/17.09 % (2472876)Termination phase: Saturation
% 117.48/17.09 % (2472876)Time elapsed: 0.790 s
% 117.48/17.09 % (2472876)Peak memory usage: 20 MB
% 117.48/17.09 % (2472876)Instructions burned: 880 (million)
% 117.48/17.09 % TRYING [8]
% 117.48/17.09 % (2472885)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2224807947:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 117.48/17.09 % (2472882)Instruction limit reached!
% 117.48/17.09 % (2472882)------------------------------
% 117.48/17.09 % (2472882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.48/17.09 % (2472882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.09 % (2472882)CaDiCaL version: 2.1.3
% 117.48/17.09 % (2472882)Termination reason: Instruction limit
% 117.48/17.09 % (2472882)Termination phase: Finite model building constraint generation
% 117.48/17.09 % (2472882)Time elapsed: 0.622 s
% 117.48/17.09 % (2472882)Peak memory usage: 49 MB
% 117.48/17.09 % (2472882)Instructions burned: 921 (million)
% 117.48/17.09 % (2472887)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1367180772:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 117.48/17.09 % TRYING [5]
% 117.48/17.09 % (2472887)Instruction limit reached!
% 117.48/17.09 % (2472887)------------------------------
% 117.48/17.09 % (2472887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.48/17.09 % (2472887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.09 % (2472887)CaDiCaL version: 2.1.3
% 117.48/17.09 % (2472887)Termination reason: Instruction limit
% 117.48/17.09 % (2472887)Termination phase: Saturation
% 117.48/17.09 % (2472887)Time elapsed: 1.389 s
% 117.48/17.09 % (2472887)Peak memory usage: 29 MB
% 117.48/17.09 % (2472887)Instructions burned: 1473 (million)
% 117.48/17.09 % (2472893)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2700050652:i=6324_2963 on theBenchmark for (2963ds/6324Mi)
% 117.48/17.09 % (2472893)Cannot represent all propositional literals internally
% 117.48/17.09 % (2472893)Refutation not found, incomplete strategy
% 285.52/40.74 % (2472893)------------------------------
% 285.52/40.74 % (2472893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 285.52/40.74 % (2472893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 285.52/40.74 % (2472893)CaDiCaL version: 2.1.3
% 285.52/40.74 % (2472893)Termination reason: Refutation not found, incomplete strategy
% 285.52/40.74 % (2472893)Time elapsed: 0.087 s
% 285.52/40.74 % (2472893)Peak memory usage: 12 MB
% 285.52/40.74 % (2472893)Instructions burned: 103 (million)
% 285.52/40.74 % (2472893)------------------------------
% 285.52/40.74 % (2472893)------------------------------
% 285.52/40.74 % (2472895)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2259418146:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 285.52/40.74 % TRYING [6]
% 285.52/40.74 % TRYING [16]
% 285.52/40.74 % TRYING [6]
% 285.52/40.74 % (2472895)Instruction limit reached!
% 285.52/40.74 % (2472895)------------------------------
% 285.52/40.74 % (2472895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 285.52/40.74 % (2472895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 285.52/40.74 % (2472895)CaDiCaL version: 2.1.3
% 285.52/40.74 % (2472895)Termination reason: Instruction limit
% 285.52/40.74 % (2472895)Termination phase: Finite model building constraint generation
% 285.52/40.74 % (2472895)Time elapsed: 1.601 s
% 285.52/40.74 % (2472895)Peak memory usage: 115 MB
% 285.52/40.74 % (2472895)Instructions burned: 2174 (million)
% 285.52/40.74 % (2472897)ott-2_1_sil=16000:newcnf=on:random_seed=517703783:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2945 on theBenchmark for (2945ds/869Mi)
% 285.52/40.74 % (2472885)Instruction limit reached!
% 285.52/40.74 % (2472885)------------------------------
% 285.52/40.74 % (2472885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 285.52/40.74 % (2472885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 285.52/40.74 % (2472885)CaDiCaL version: 2.1.3
% 285.52/40.74 % (2472885)Termination reason: Instruction limit
% 285.52/40.74 % (2472885)Termination phase: Saturation
% 285.52/40.74 % (2472885)Time elapsed: 4.170 s
% 285.52/40.74 % (2472885)Peak memory usage: 44 MB
% 285.52/40.74 % (2472885)Instructions burned: 5132 (million)
% 285.52/40.74 % (2472899)ott+10_1_sil=32000:tgt=ground:random_seed=1703109041:i=5114:av=off_2941 on theBenchmark for (2941ds/5114Mi)
% 285.52/40.74 % (2472897)Instruction limit reached!
% 285.52/40.74 % (2472897)------------------------------
% 285.52/40.74 % (2472897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 285.52/40.74 % (2472897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 285.52/40.74 % (2472897)CaDiCaL version: 2.1.3
% 285.52/40.74 % (2472897)Termination reason: Instruction limit
% 285.52/40.74 % (2472897)Termination phase: Saturation
% 285.52/40.74 % (2472897)Time elapsed: 0.862 s
% 285.52/40.74 % (2472897)Peak memory usage: 19 MB
% 285.52/40.74 % (2472897)Instructions burned: 869 (million)
% 285.52/40.74 % (2472901)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=512781946:i=54282_2936 on theBenchmark for (2936ds/54282Mi)
% 285.52/40.74 % TRYING [1]
% 285.52/40.74 % TRYING [2]
% 285.52/40.74 % TRYING [3]
% 285.52/40.74 % TRYING [4]
% 285.52/40.74 % TRYING [5]
% 285.52/40.74 % (2472881)Instruction limit reached!
% 285.52/40.74 % (2472881)------------------------------
% 285.52/40.74 % (2472881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 285.52/40.74 % (2472881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 285.52/40.74 % (2472881)CaDiCaL version: 2.1.3
% 285.52/40.74 % (2472881)Termination reason: Instruction limit
% 285.52/40.74 % (2472881)Termination phase: Finite model building constraint generation
% 285.52/40.74 % (2472881)Time elapsed: 6.747 s
% 285.52/40.74 % (2472881)Peak memory usage: 580 MB
% 285.52/40.74 % (2472881)Instructions burned: 9515 (million)
% 285.52/40.74 % (2472907)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2365243358:i=3512:aac=none_2915 on theBenchmark for (2915ds/3512Mi)
% 285.52/40.74 % TRYING [6]
% 285.52/40.74 % (2472879)Instruction limit reached!
% 285.52/40.74 % (2472879)------------------------------
% 285.52/40.74 % (2472879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 285.52/40.74 % (2472879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 285.52/40.74 % (2472879)CaDiCaL version: 2.1.3
% 285.52/40.74 % (2472879)Termination reason: Instruction limit
% 285.52/40.74 % (2472879)Termination phase: Finite model building SAT solving
% 285.52/40.74 % (2472879)Time elapsed: 8.827 s
% 285.52/40.74 % (2472879)Peak memory usage: 187 MB
% 285.52/40.74 % (2472879)Instructions burned: 22063 (million)
% 285.52/40.74 % (2472909)dis+21_1_sil=32000:sas=cadical:random_seed=4110381862:i=3773:amm=off_2898 on theBenchmark for (2898ds/3773Mi)
% 154.11/41.85 % (2472899)Instruction limit reached!
% 154.11/41.85 % (2472899)------------------------------
% 154.11/41.85 % (2472899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472899)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472899)Termination reason: Instruction limit
% 154.11/41.85 % (2472899)Termination phase: Saturation
% 154.11/41.85 % (2472899)Time elapsed: 4.492 s
% 154.11/41.85 % (2472899)Peak memory usage: 54 MB
% 154.11/41.85 % (2472899)Instructions burned: 5114 (million)
% 154.11/41.85 % (2472911)ott+11_1_sil=16000:gs=on:random_seed=2175237592:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2895 on theBenchmark for (2895ds/2251Mi)
% 154.11/41.85 % (2472907)Instruction limit reached!
% 154.11/41.85 % (2472907)------------------------------
% 154.11/41.85 % (2472907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472907)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472907)Termination reason: Instruction limit
% 154.11/41.85 % (2472907)Termination phase: Saturation
% 154.11/41.85 % (2472907)Time elapsed: 3.040 s
% 154.11/41.85 % (2472907)Peak memory usage: 37 MB
% 154.11/41.85 % (2472907)Instructions burned: 3513 (million)
% 154.11/41.85 % (2472913)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=356758881:fmbsr=1.6:i=67534_2884 on theBenchmark for (2884ds/67534Mi)
% 154.11/41.85 % (2472911)Instruction limit reached!
% 154.11/41.85 % (2472911)------------------------------
% 154.11/41.85 % (2472911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472911)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472911)Termination reason: Instruction limit
% 154.11/41.85 % (2472911)Termination phase: Saturation
% 154.11/41.85 % (2472911)Time elapsed: 1.387 s
% 154.11/41.85 % (2472911)Peak memory usage: 43 MB
% 154.11/41.85 % (2472911)Instructions burned: 2252 (million)
% 154.11/41.85 % (2472915)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2837145417:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2881 on theBenchmark for (2881ds/4591Mi)
% 154.11/41.85 % TRYING [7]
% 154.11/41.85 % (2472909)Instruction limit reached!
% 154.11/41.85 % (2472909)------------------------------
% 154.11/41.85 % (2472909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472909)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472909)Termination reason: Instruction limit
% 154.11/41.85 % (2472909)Termination phase: Saturation
% 154.11/41.85 % (2472909)Time elapsed: 2.862 s
% 154.11/41.85 % (2472909)Peak memory usage: 40 MB
% 154.11/41.85 % (2472909)Instructions burned: 3773 (million)
% 154.11/41.85 % (2472917)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3086388572:i=29340_2869 on theBenchmark for (2869ds/29340Mi)
% 154.11/41.85 % (2472915)Instruction limit reached!
% 154.11/41.85 % (2472915)------------------------------
% 154.11/41.85 % (2472915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472915)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472915)Termination reason: Instruction limit
% 154.11/41.85 % (2472915)Termination phase: Saturation
% 154.11/41.85 % (2472915)Time elapsed: 2.146 s
% 154.11/41.85 % (2472915)Peak memory usage: 39 MB
% 154.11/41.85 % (2472915)Instructions burned: 4592 (million)
% 154.11/41.85 % (2472919)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=87987136:i=5211_2860 on theBenchmark for (2860ds/5211Mi)
% 154.11/41.85 % (2472919)Instruction limit reached!
% 154.11/41.85 % (2472919)------------------------------
% 154.11/41.85 % (2472919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472919)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472919)Termination reason: Instruction limit
% 154.11/41.85 % (2472919)Termination phase: Saturation
% 154.11/41.85 % (2472919)Time elapsed: 2.510 s
% 154.11/41.85 % (2472919)Peak memory usage: 49 MB
% 154.11/41.85 % (2472919)Instructions burned: 5212 (million)
% 154.11/41.85 % (2472921)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1394914817:i=5497:nm=2_2834 on theBenchmark for (2834ds/5497Mi)
% 154.11/41.85 % TRYING [17]
% 154.11/41.85 % TRYING [7]
% 154.11/41.85 % (2472921)Instruction limit reached!
% 154.11/41.85 % (2472921)------------------------------
% 154.11/41.85 % (2472921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472921)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472921)Termination reason: Instruction limit
% 154.11/41.85 % (2472921)Termination phase: Finite model building constraint generation
% 154.11/41.85 % (2472921)Time elapsed: 1.216 s
% 154.11/41.85 % (2472921)Peak memory usage: 312 MB
% 154.11/41.85 % (2472921)Instructions burned: 5502 (million)
% 154.11/41.85 % (2472966)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=696522173:fmbsr=2:i=46332_2821 on theBenchmark for (2821ds/46332Mi)
% 154.11/41.85 % TRYING [15]
% 154.11/41.85 % TRYING [7]
% 154.11/41.85 % (2472966)Instruction limit reached!
% 154.11/41.85 % (2472966)------------------------------
% 154.11/41.85 % (2472966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472966)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472966)Termination reason: Instruction limit
% 154.11/41.85 % (2472966)Termination phase: Finite model building constraint generation
% 154.11/41.85 % (2472966)Time elapsed: 8.307 s
% 154.11/41.85 % (2472966)Peak memory usage: 1845 MB
% 154.11/41.85 % (2472966)Instructions burned: 46334 (million)
% 154.11/41.85 % (2473082)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2065990984:i=14071_2737 on theBenchmark for (2737ds/14071Mi)
% 154.11/41.85 % TRYING [12]
% 154.11/41.85 % (2473082)Instruction limit reached!
% 154.11/41.85 % (2473082)------------------------------
% 154.11/41.85 % (2473082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2473082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2473082)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2473082)Termination reason: Instruction limit
% 154.11/41.85 % (2473082)Termination phase: Finite model building constraint generation
% 154.11/41.85 % (2473082)Time elapsed: 2.561 s
% 154.11/41.85 % (2473082)Peak memory usage: 660 MB
% 154.11/41.85 % (2473082)Instructions burned: 14076 (million)
% 154.11/41.85 % (2473245)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3898428433:i=22565:add=on:rawr=on_2710 on theBenchmark for (2710ds/22565Mi)
% 154.11/41.85 % (2472917)Instruction limit reached!
% 154.11/41.85 % (2472917)------------------------------
% 154.11/41.85 % (2472917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472917)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472917)Termination reason: Instruction limit
% 154.11/41.85 % (2472917)Termination phase: Saturation
% 154.11/41.85 % (2472917)Time elapsed: 17.533 s
% 154.11/41.85 % (2472917)Peak memory usage: 813 MB
% 154.11/41.85 % (2472917)Instructions burned: 29342 (million)
% 154.11/41.85 % (2473762)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=542628737:i=8173:av=off_2692 on theBenchmark for (2692ds/8173Mi)
% 154.11/41.85 % (2473762)Instruction limit reached!
% 154.11/41.85 % (2473762)------------------------------
% 154.11/41.85 % (2473762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2473762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2473762)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2473762)Termination reason: Instruction limit
% 154.11/41.85 % (2473762)Termination phase: Saturation
% 154.11/41.85 % (2473762)Time elapsed: 6.804 s
% 154.11/41.85 % (2473762)Peak memory usage: 122 MB
% 154.11/41.85 % (2473762)Instructions burned: 8173 (million)
% 154.11/41.85 % (2473937)dis+10_16:1_sil=16000:random_seed=274377658:i=9155:fsr=off_2624 on theBenchmark for (2624ds/9155Mi)
% 154.11/41.85 % (2472901)Instruction limit reached!
% 154.11/41.85 % (2472901)------------------------------
% 154.11/41.85 % (2472901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2472901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2472901)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2472901)Termination reason: Instruction limit
% 154.11/41.85 % (2472901)Termination phase: Finite model building SAT solving
% 154.11/41.85 % (2472901)Time elapsed: 33.654 s
% 154.11/41.85 % (2472901)Peak memory usage: 793 MB
% 154.11/41.85 % (2472901)Instructions burned: 54282 (million)
% 154.11/41.85 % (2473939)ott-3_8_sil=64000:random_seed=2417740377:i=20139:bs=on_2598 on theBenchmark for (2598ds/20139Mi)
% 154.11/41.85 % (2473937) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2472840-2473937"...
% 154.11/41.85 % (2473937)...printing done.
% 154.11/41.85 % (2473245)Instruction limit reached!
% 154.11/41.85 % (2473245)------------------------------
% 154.11/41.85 % (2473245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.85 % (2473245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.85 % (2473245)CaDiCaL version: 2.1.3
% 154.11/41.85 % (2473245)Termination reason: Instruction limit
% 154.11/41.85 % (2473245)Termination phase: Saturation
% 154.11/41.85 % (2473245)Time elapsed: 12.220 s
% 154.11/41.85 % (2473245)Peak memory usage: 147 MB
% 154.11/41.85 % (2473245)Instructions burned: 22565 (million)
% 154.11/41.85 % (2473937)Refutation found. Thanks to Tanya!
% 154.11/41.85 % SZS status Theorem for theBenchmark
% 154.11/41.85 % SZS output start Proof for theBenchmark
% See solution above
% 154.11/41.86 % (2473937)------------------------------
% 154.11/41.86 % (2473937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.11/41.86 % (2473937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.11/41.86 % (2473937)CaDiCaL version: 2.1.3
% 154.11/41.86 % (2473937)Termination reason: Refutation
% 154.11/41.86 % (2473937)Time elapsed: 3.512 s
% 154.11/41.86 % (2473937)Peak memory usage: 50 MB
% 154.11/41.86 % (2473937)Instructions burned: 3882 (million)
% 154.11/41.86 % (2472840)Success in time 41.34 s
% 154.11/41.86 % Vampire exiting
%------------------------------------------------------------------------------