%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT348+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:10 AM UTC 2026
% Result : Theorem 21.81s 7.18s
% Output : Refutation 44.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 48
% Syntax : Number of formulae : 335 ( 51 unt; 19 def)
% Number of atoms : 1241 ( 95 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 1602 ( 696 ~; 698 |; 156 &)
% ( 20 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 44 ( 42 usr; 20 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 3 con; 0-2 aty)
% Number of variables : 144 ( 0 sgn 142 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1257,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(f2965,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f5433,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f6157,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f6159,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_orders_2(X0)
=> X0 = g1_orders_2(u1_struct_0(X0),u1_orders_2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v1_orders_2) ).
fof(f6167,axiom,
! [X0] :
( l1_orders_2(X0)
=> m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_orders_2) ).
fof(f6168,axiom,
! [X0,X1] :
( m1_relset_1(X1,X0,X0)
=> ( v1_orders_2(g1_orders_2(X0,X1))
& l1_orders_2(g1_orders_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_g1_orders_2) ).
fof(f6769,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_lattice3) ).
fof(f6770,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice3) ).
fof(f6848,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_lattice3) ).
fof(f7454,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& l1_orders_2(X0) )
=> ( r2_yellow_0(X0,k1_xboole_0)
& r1_yellow_0(X0,u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t43_yellow_0) ).
fof(f7455,axiom,
! [X0] :
( l1_orders_2(X0)
=> k3_yellow_0(X0) = k1_yellow_0(X0,k1_xboole_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_yellow_0) ).
fof(f7456,axiom,
! [X0] :
( l1_orders_2(X0)
=> k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_yellow_0) ).
fof(f7497,axiom,
! [X0] :
( l1_orders_2(X0)
=> m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow_0) ).
fof(f7498,axiom,
! [X0] :
( l1_orders_2(X0)
=> m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_yellow_0) ).
fof(f7722,axiom,
! [X0] : k3_yellow_1(X0) = k2_yellow_1(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_yellow_1) ).
fof(f8406,axiom,
! [X0] :
( ( v2_orders_2(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_yellow_7) ).
fof(f8407,axiom,
! [X0] :
( ( v3_orders_2(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_yellow_7) ).
fof(f8408,axiom,
! [X0] :
( ( v4_orders_2(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_yellow_7) ).
fof(f8410,axiom,
! [X0] :
( ( v2_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_yellow_7) ).
fof(f8415,axiom,
! [X0] :
( ( v2_yellow_0(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc10_yellow_7) ).
fof(f8433,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( r2_yellow_0(X0,X1)
| r1_yellow_0(k7_lattice3(X0),X1) )
=> k2_yellow_0(X0,X1) = k1_yellow_0(k7_lattice3(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_yellow_7) ).
fof(f8440,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k7_lattice3(X0)))
=> ( X1 = X2
=> ( k6_waybel_0(X0,X1) = k7_waybel_0(k7_lattice3(X0),X2)
& k7_waybel_0(X0,X1) = k6_waybel_0(k7_lattice3(X0),X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_yellow_7) ).
fof(f8648,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v1_yellow_0(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k2_yellow_1(k8_waybel_0(X0)))
& v4_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v7_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v4_waybel_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& m1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_waybel13) ).
fof(f8690,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v1_yellow_0(X0)
& l1_orders_2(X0) )
=> k7_waybel_0(X0,k3_yellow_0(X0)) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_waybel14) ).
fof(f8691,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& l1_orders_2(X0) )
=> k6_waybel_0(X0,k4_yellow_0(X0)) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_waybel14) ).
fof(f8776,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_lattice3(X0)
& v2_yellow_0(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_waybel16) ).
fof(f8783,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& l1_orders_2(X0) )
=> k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_waybel16) ).
fof(f8955,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v4_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v7_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v4_waybel_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& m1_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_waybel22) ).
fof(f8956,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v4_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v7_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v4_waybel_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& m1_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0))) ) ),
inference(negated_conjecture,[status(cth)],[f8955]) ).
fof(f9011,plain,
? [X0] :
( ( v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
| ~ v4_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ v7_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ v4_waybel_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ m1_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8956]) ).
fof(f9012,plain,
? [X0] :
( ( v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
| ~ v4_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ v7_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ v4_waybel_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ m1_yellow_0(k2_yellow_1(k9_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f9011]) ).
fof(f9038,plain,
! [X0] :
( k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8783]) ).
fof(f9039,plain,
! [X0] :
( k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9038]) ).
fof(f9040,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0))) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8776]) ).
fof(f9041,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0))) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9040]) ).
fof(f9106,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0)) )
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8415]) ).
fof(f9107,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0)) )
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9106]) ).
fof(f9209,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(k8_waybel_0(X0)))
& v4_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v7_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v4_waybel_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& m1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0))) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8648]) ).
fof(f9210,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(k8_waybel_0(X0)))
& v4_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v7_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& v4_waybel_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
& m1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0))) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9209]) ).
fof(f9317,plain,
! [X0] :
( k7_waybel_0(X0,k3_yellow_0(X0)) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8690]) ).
fof(f9318,plain,
! [X0] :
( k7_waybel_0(X0,k3_yellow_0(X0)) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9317]) ).
fof(f9331,plain,
! [X0] :
( m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7497]) ).
fof(f9334,plain,
! [X0] :
( k3_yellow_0(X0) = k1_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7455]) ).
fof(f9337,plain,
! [X0] :
( k6_waybel_0(X0,k4_yellow_0(X0)) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8691]) ).
fof(f9338,plain,
! [X0] :
( k6_waybel_0(X0,k4_yellow_0(X0)) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9337]) ).
fof(f9347,plain,
! [X0] :
( m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7498]) ).
fof(f9350,plain,
! [X0] :
( k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7456]) ).
fof(f9386,plain,
! [X0] :
( ! [X1] :
( k2_yellow_0(X0,X1) = k1_yellow_0(k7_lattice3(X0),X1)
| ( ~ r2_yellow_0(X0,X1)
& ~ r1_yellow_0(k7_lattice3(X0),X1) ) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8433]) ).
fof(f9387,plain,
! [X0] :
( ! [X1] :
( k2_yellow_0(X0,X1) = k1_yellow_0(k7_lattice3(X0),X1)
| ( ~ r2_yellow_0(X0,X1)
& ~ r1_yellow_0(k7_lattice3(X0),X1) ) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9386]) ).
fof(f9410,plain,
! [X0] :
( ( r2_yellow_0(X0,k1_xboole_0)
& r1_yellow_0(X0,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7454]) ).
fof(f9411,plain,
! [X0] :
( ( r2_yellow_0(X0,k1_xboole_0)
& r1_yellow_0(X0,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9410]) ).
fof(f9431,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0)) )
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8410]) ).
fof(f9432,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0)) )
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9431]) ).
fof(f9433,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8408]) ).
fof(f9434,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9433]) ).
fof(f9435,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0)) )
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8407]) ).
fof(f9436,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0)) )
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9435]) ).
fof(f9437,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8406]) ).
fof(f9438,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9437]) ).
fof(f9439,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6848]) ).
fof(f9441,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6770]) ).
fof(f9442,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9441]) ).
fof(f9443,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6769]) ).
fof(f9444,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9443]) ).
fof(f9843,plain,
! [X0] :
( m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6167]) ).
fof(f9984,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6157]) ).
fof(f10211,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k6_waybel_0(X0,X1) = k7_waybel_0(k7_lattice3(X0),X2)
& k7_waybel_0(X0,X1) = k6_waybel_0(k7_lattice3(X0),X2) )
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k7_lattice3(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8440]) ).
fof(f10212,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k6_waybel_0(X0,X1) = k7_waybel_0(k7_lattice3(X0),X2)
& k7_waybel_0(X0,X1) = k6_waybel_0(k7_lattice3(X0),X2) )
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k7_lattice3(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f10211]) ).
fof(f10856,plain,
! [X0,X1] :
( ( v1_orders_2(g1_orders_2(X0,X1))
& l1_orders_2(g1_orders_2(X0,X1)) )
| ~ m1_relset_1(X1,X0,X0) ),
inference(ennf_transformation,[],[f6168]) ).
fof(f10857,plain,
! [X0] :
( X0 = g1_orders_2(u1_struct_0(X0),u1_orders_2(X0))
| ~ v1_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6159]) ).
fof(f10858,plain,
! [X0] :
( X0 = g1_orders_2(u1_struct_0(X0),u1_orders_2(X0))
| ~ v1_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f10857]) ).
fof(f11539,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f5433]) ).
fof(f11929,plain,
( ( v3_struct_0(k2_yellow_1(k9_waybel_0(sK19)))
| ~ v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k3_yellow_1(u1_struct_0(sK19)))
| ~ v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k3_yellow_1(u1_struct_0(sK19)))
| ~ v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k3_yellow_1(u1_struct_0(sK19)))
| ~ m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k3_yellow_1(u1_struct_0(sK19))) )
& ~ v3_struct_0(sK19)
& v2_orders_2(sK19)
& v3_orders_2(sK19)
& v4_orders_2(sK19)
& v2_yellow_0(sK19)
& v2_lattice3(sK19)
& l1_orders_2(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X0,sK19)],[f9012]) ).
fof(f11944,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,[],[f1257]) ).
fof(f12874,plain,
l1_orders_2(sK19),
inference(cnf_transformation,[],[f11929]) ).
fof(f12875,plain,
v2_lattice3(sK19),
inference(cnf_transformation,[],[f11929]) ).
fof(f12876,plain,
v2_yellow_0(sK19),
inference(cnf_transformation,[],[f11929]) ).
fof(f12877,plain,
v4_orders_2(sK19),
inference(cnf_transformation,[],[f11929]) ).
fof(f12878,plain,
v3_orders_2(sK19),
inference(cnf_transformation,[],[f11929]) ).
fof(f12879,plain,
v2_orders_2(sK19),
inference(cnf_transformation,[],[f11929]) ).
fof(f12880,plain,
~ v3_struct_0(sK19),
inference(cnf_transformation,[],[f11929]) ).
fof(f12881,plain,
( v3_struct_0(k2_yellow_1(k9_waybel_0(sK19)))
| ~ v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k3_yellow_1(u1_struct_0(sK19)))
| ~ v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k3_yellow_1(u1_struct_0(sK19)))
| ~ v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k3_yellow_1(u1_struct_0(sK19)))
| ~ m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k3_yellow_1(u1_struct_0(sK19))) ),
inference(cnf_transformation,[],[f11929]) ).
fof(f12913,plain,
! [X0] : k3_yellow_1(X0) = k2_yellow_1(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f7722]) ).
fof(f12928,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f11944]) ).
fof(f12952,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f9039]) ).
fof(f12962,plain,
! [X0] :
( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9041]) ).
fof(f13081,plain,
! [X0] :
( v1_yellow_0(k7_lattice3(X0))
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9107]) ).
fof(f13252,plain,
! [X0] :
( m1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9210]) ).
fof(f13253,plain,
! [X0] :
( v4_waybel_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9210]) ).
fof(f13254,plain,
! [X0] :
( v7_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9210]) ).
fof(f13255,plain,
! [X0] :
( v4_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k3_yellow_1(u1_struct_0(X0)))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9210]) ).
fof(f13503,plain,
! [X0] :
( ~ v1_yellow_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| u1_struct_0(X0) = k7_waybel_0(X0,k3_yellow_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9318]) ).
fof(f13513,plain,
! [X0] :
( m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9331]) ).
fof(f13515,plain,
! [X0] :
( k3_yellow_0(X0) = k1_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9334]) ).
fof(f13517,plain,
! [X0] :
( ~ v2_yellow_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| u1_struct_0(X0) = k6_waybel_0(X0,k4_yellow_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9338]) ).
fof(f13523,plain,
! [X0] :
( ~ l1_orders_2(X0)
| m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f9347]) ).
fof(f13525,plain,
! [X0] :
( k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9350]) ).
fof(f13566,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ r2_yellow_0(X0,X1)
| v3_struct_0(X0)
| k2_yellow_0(X0,X1) = k1_yellow_0(k7_lattice3(X0),X1) ),
inference(cnf_transformation,[],[f9387]) ).
fof(f13624,plain,
! [X0] :
( r2_yellow_0(X0,k1_xboole_0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9411]) ).
fof(f13668,plain,
! [X0] :
( v1_lattice3(k7_lattice3(X0))
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9432]) ).
fof(f13671,plain,
! [X0] :
( v4_orders_2(k7_lattice3(X0))
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9434]) ).
fof(f13673,plain,
! [X0] :
( v3_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9436]) ).
fof(f13675,plain,
! [X0] :
( v2_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9438]) ).
fof(f13677,plain,
! [X0] :
( l1_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9439]) ).
fof(f13682,plain,
! [X0] :
( ~ v3_struct_0(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9442]) ).
fof(f13686,plain,
! [X0] :
( v1_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9444]) ).
fof(f14350,plain,
! [X0] :
( m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9843]) ).
fof(f14498,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9984]) ).
fof(f14845,plain,
! [X2,X0,X1] :
( k6_waybel_0(X0,X1) = k7_waybel_0(k7_lattice3(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k7_lattice3(X0)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f10212]) ).
fof(f15786,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f2965]) ).
fof(f15879,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,X0,X0)
| l1_orders_2(g1_orders_2(X0,X1)) ),
inference(cnf_transformation,[],[f10856]) ).
fof(f15881,plain,
! [X0] :
( ~ v1_orders_2(X0)
| g1_orders_2(u1_struct_0(X0),u1_orders_2(X0)) = X0
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f10858]) ).
fof(f16980,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f11539]) ).
fof(f17380,plain,
( v3_struct_0(k2_yellow_1(k9_waybel_0(sK19)))
| ~ v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19))))
| ~ v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19))))
| ~ v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19))))
| ~ m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19)))) ),
inference(definition_unfolding,[],[f12881,f12913,f12913,f12913,f12913]) ).
fof(f17450,plain,
! [X0] :
( v4_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(X0))))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f13255,f12913]) ).
fof(f17451,plain,
! [X0] :
( ~ v1_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| v7_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(X0))))
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f13254,f12913]) ).
fof(f17452,plain,
! [X0] :
( ~ v1_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| v4_waybel_0(k2_yellow_1(k8_waybel_0(X0)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(X0))))
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f13253,f12913]) ).
fof(f17453,plain,
! [X0] :
( ~ v1_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| m1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(X0))))
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f13252,f12913]) ).
fof(f17529,plain,
! [X0] :
( ~ l1_orders_2(X0)
| k3_yellow_0(X0) = k1_yellow_0(X0,np__0) ),
inference(definition_unfolding,[],[f13515,f15786]) ).
fof(f17531,plain,
! [X0] :
( ~ l1_orders_2(X0)
| k4_yellow_0(X0) = k2_yellow_0(X0,np__0) ),
inference(definition_unfolding,[],[f13525,f15786]) ).
fof(f17563,plain,
! [X0] :
( r2_yellow_0(X0,np__0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f13624,f15786]) ).
fof(f18952,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,u1_struct_0(k7_lattice3(X0)))
| k6_waybel_0(X0,X2) = k7_waybel_0(k7_lattice3(X0),X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f14845]) ).
fof(f19439,definition,
( spl588_13
<=> m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19)))) ),
introduced(definition,[new_symbols(definition,[spl588_13])],[avatar_definition]) ).
fof(f19440,plain,
( ~ m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19))))
| spl588_13 ),
inference(avatar_component_clause,[],[f19439]) ).
fof(f19442,definition,
( spl588_14
<=> v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19)))) ),
introduced(definition,[new_symbols(definition,[spl588_14])],[avatar_definition]) ).
fof(f19443,plain,
( ~ v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19))))
| spl588_14 ),
inference(avatar_component_clause,[],[f19442]) ).
fof(f19445,definition,
( spl588_15
<=> v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19)))) ),
introduced(definition,[new_symbols(definition,[spl588_15])],[avatar_definition]) ).
fof(f19446,plain,
( ~ v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19))))
| spl588_15 ),
inference(avatar_component_clause,[],[f19445]) ).
fof(f19448,definition,
( spl588_16
<=> v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19)))) ),
introduced(definition,[new_symbols(definition,[spl588_16])],[avatar_definition]) ).
fof(f19449,plain,
( ~ v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(sK19))))
| spl588_16 ),
inference(avatar_component_clause,[],[f19448]) ).
fof(f19451,definition,
( spl588_17
<=> v3_struct_0(k2_yellow_1(k9_waybel_0(sK19))) ),
introduced(definition,[new_symbols(definition,[spl588_17])],[avatar_definition]) ).
fof(f19452,plain,
( v3_struct_0(k2_yellow_1(k9_waybel_0(sK19)))
| ~ spl588_17 ),
inference(avatar_component_clause,[],[f19451]) ).
fof(f19453,plain,
( ~ spl588_13
| ~ spl588_14
| ~ spl588_15
| ~ spl588_16
| spl588_17 ),
inference(avatar_split_clause,[],[f17380,f19451,f19448,f19445,f19442,f19439]) ).
fof(f19554,plain,
( v3_struct_0(sK19)
| ~ v2_orders_2(sK19)
| ~ v3_orders_2(sK19)
| k9_waybel_0(sK19) = k8_waybel_0(k7_lattice3(sK19)) ),
inference(resolution,[],[f12952,f12874]) ).
fof(f19555,plain,
( ~ v2_orders_2(sK19)
| ~ v3_orders_2(sK19)
| k9_waybel_0(sK19) = k8_waybel_0(k7_lattice3(sK19)) ),
inference(forward_subsumption_resolution,[],[f19554,f12880]) ).
fof(f19556,plain,
( ~ v3_orders_2(sK19)
| k9_waybel_0(sK19) = k8_waybel_0(k7_lattice3(sK19)) ),
inference(forward_subsumption_resolution,[],[f19555,f12879]) ).
fof(f19557,plain,
k9_waybel_0(sK19) = k8_waybel_0(k7_lattice3(sK19)),
inference(forward_subsumption_resolution,[],[f19556,f12878]) ).
fof(f19567,plain,
( v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ v2_orders_2(k7_lattice3(sK19))
| ~ v3_orders_2(k7_lattice3(sK19))
| ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| ~ v1_yellow_0(k7_lattice3(sK19))
| ~ l1_orders_2(k7_lattice3(sK19)) ),
inference(superposition,[],[f17450,f19557]) ).
fof(f19577,plain,
! [X0] :
( ~ l1_orders_2(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f16980,f14498]) ).
fof(f19583,plain,
( v3_struct_0(sK19)
| ~ v4_orders_2(sK19)
| u1_struct_0(sK19) = k6_waybel_0(sK19,k4_yellow_0(sK19))
| ~ l1_orders_2(sK19) ),
inference(resolution,[],[f13517,f12876]) ).
fof(f19614,definition,
( spl588_18
<=> l1_orders_2(k7_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl588_18])],[avatar_definition]) ).
fof(f19615,plain,
( ~ l1_orders_2(k7_lattice3(sK19))
| spl588_18 ),
inference(avatar_component_clause,[],[f19614]) ).
fof(f19617,definition,
( spl588_19
<=> v1_yellow_0(k7_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl588_19])],[avatar_definition]) ).
fof(f19618,plain,
( ~ v1_yellow_0(k7_lattice3(sK19))
| spl588_19 ),
inference(avatar_component_clause,[],[f19617]) ).
fof(f19620,definition,
( spl588_20
<=> v1_lattice3(k7_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl588_20])],[avatar_definition]) ).
fof(f19621,plain,
( ~ v1_lattice3(k7_lattice3(sK19))
| spl588_20 ),
inference(avatar_component_clause,[],[f19620]) ).
fof(f19623,definition,
( spl588_21
<=> v4_orders_2(k7_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl588_21])],[avatar_definition]) ).
fof(f19624,plain,
( ~ v4_orders_2(k7_lattice3(sK19))
| spl588_21 ),
inference(avatar_component_clause,[],[f19623]) ).
fof(f19626,definition,
( spl588_22
<=> v3_orders_2(k7_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl588_22])],[avatar_definition]) ).
fof(f19627,plain,
( ~ v3_orders_2(k7_lattice3(sK19))
| spl588_22 ),
inference(avatar_component_clause,[],[f19626]) ).
fof(f19629,definition,
( spl588_23
<=> v2_orders_2(k7_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl588_23])],[avatar_definition]) ).
fof(f19630,plain,
( ~ v2_orders_2(k7_lattice3(sK19))
| spl588_23 ),
inference(avatar_component_clause,[],[f19629]) ).
fof(f19632,definition,
( spl588_24
<=> v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19))))) ),
introduced(definition,[new_symbols(definition,[spl588_24])],[avatar_definition]) ).
fof(f19633,plain,
( v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ spl588_24 ),
inference(avatar_component_clause,[],[f19632]) ).
fof(f19634,plain,
( ~ spl588_18
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23
| spl588_24 ),
inference(avatar_split_clause,[],[f19567,f19632,f19629,f19626,f19623,f19620,f19617,f19614]) ).
fof(f19640,plain,
( ~ v4_orders_2(sK19)
| u1_struct_0(sK19) = k6_waybel_0(sK19,k4_yellow_0(sK19))
| ~ l1_orders_2(sK19) ),
inference(forward_subsumption_resolution,[],[f19583,f12880]) ).
fof(f19664,definition,
( spl588_31
<=> v3_struct_0(k7_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl588_31])],[avatar_definition]) ).
fof(f19665,plain,
( v3_struct_0(k7_lattice3(sK19))
| ~ spl588_31 ),
inference(avatar_component_clause,[],[f19664]) ).
fof(f19683,plain,
( u1_struct_0(sK19) = k6_waybel_0(sK19,k4_yellow_0(sK19))
| ~ l1_orders_2(sK19) ),
inference(forward_subsumption_resolution,[],[f19640,f12877]) ).
fof(f19693,plain,
u1_struct_0(sK19) = k6_waybel_0(sK19,k4_yellow_0(sK19)),
inference(forward_subsumption_resolution,[],[f19683,f12874]) ).
fof(f19725,plain,
( ~ l1_orders_2(sK19)
| spl588_18 ),
inference(resolution,[],[f19615,f13677]) ).
fof(f19727,plain,
( $false
| spl588_18 ),
inference(forward_subsumption_resolution,[],[f19725,f12874]) ).
fof(f19728,plain,
spl588_18,
inference(avatar_contradiction_clause,[],[f19727]) ).
fof(f19730,plain,
( ~ v3_orders_2(sK19)
| ~ l1_orders_2(sK19)
| spl588_22 ),
inference(resolution,[],[f19627,f13673]) ).
fof(f19732,plain,
( ~ l1_orders_2(sK19)
| spl588_22 ),
inference(forward_subsumption_resolution,[],[f19730,f12878]) ).
fof(f19733,plain,
( $false
| spl588_22 ),
inference(forward_subsumption_resolution,[],[f19732,f12874]) ).
fof(f19734,plain,
spl588_22,
inference(avatar_contradiction_clause,[],[f19733]) ).
fof(f19736,plain,
( ~ v2_orders_2(sK19)
| ~ l1_orders_2(sK19)
| spl588_23 ),
inference(resolution,[],[f19630,f13675]) ).
fof(f19738,plain,
( ~ l1_orders_2(sK19)
| spl588_23 ),
inference(forward_subsumption_resolution,[],[f19736,f12879]) ).
fof(f19739,plain,
( $false
| spl588_23 ),
inference(forward_subsumption_resolution,[],[f19738,f12874]) ).
fof(f19740,plain,
spl588_23,
inference(avatar_contradiction_clause,[],[f19739]) ).
fof(f19742,plain,
( ~ v4_orders_2(sK19)
| ~ l1_orders_2(sK19)
| spl588_21 ),
inference(resolution,[],[f19624,f13671]) ).
fof(f19744,plain,
( ~ l1_orders_2(sK19)
| spl588_21 ),
inference(forward_subsumption_resolution,[],[f19742,f12877]) ).
fof(f19745,plain,
( $false
| spl588_21 ),
inference(forward_subsumption_resolution,[],[f19744,f12874]) ).
fof(f19746,plain,
spl588_21,
inference(avatar_contradiction_clause,[],[f19745]) ).
fof(f19747,plain,
u1_struct_0(sK19) = k2_pre_topc(sK19),
inference(resolution,[],[f19577,f12874]) ).
fof(f19749,plain,
! [X0] :
( ~ l1_orders_2(X0)
| u1_struct_0(k7_lattice3(X0)) = k2_pre_topc(k7_lattice3(X0)) ),
inference(resolution,[],[f19577,f13677]) ).
fof(f19750,plain,
( ~ v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(sK19))))
| spl588_16 ),
inference(superposition,[],[f19449,f19747]) ).
fof(f20063,plain,
( ~ v2_lattice3(sK19)
| ~ l1_orders_2(sK19)
| spl588_20 ),
inference(resolution,[],[f13668,f19621]) ).
fof(f20067,plain,
( ~ l1_orders_2(sK19)
| spl588_20 ),
inference(forward_subsumption_resolution,[],[f20063,f12875]) ).
fof(f20069,plain,
( $false
| spl588_20 ),
inference(forward_subsumption_resolution,[],[f20067,f12874]) ).
fof(f20070,plain,
spl588_20,
inference(avatar_contradiction_clause,[],[f20069]) ).
fof(f20072,plain,
( ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19)
| spl588_19 ),
inference(resolution,[],[f19618,f13081]) ).
fof(f20074,plain,
( ~ l1_orders_2(sK19)
| spl588_19 ),
inference(forward_subsumption_resolution,[],[f20072,f12876]) ).
fof(f20075,plain,
( $false
| spl588_19 ),
inference(forward_subsumption_resolution,[],[f20074,f12874]) ).
fof(f20076,plain,
spl588_19,
inference(avatar_contradiction_clause,[],[f20075]) ).
fof(f20188,plain,
m1_subset_1(k4_yellow_0(sK19),u1_struct_0(sK19)),
inference(resolution,[],[f13523,f12874]) ).
fof(f20192,plain,
m1_subset_1(k4_yellow_0(sK19),k2_pre_topc(sK19)),
inference(forward_demodulation,[],[f20188,f19747]) ).
fof(f20211,plain,
! [X0] :
( ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| k7_lattice3(X0) = g1_orders_2(u1_struct_0(k7_lattice3(X0)),u1_orders_2(k7_lattice3(X0)))
| ~ l1_orders_2(k7_lattice3(X0)) ),
inference(resolution,[],[f13686,f15881]) ).
fof(f20212,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_orders_2(X0)
| k7_lattice3(X0) = g1_orders_2(u1_struct_0(k7_lattice3(X0)),u1_orders_2(k7_lattice3(X0))) ),
inference(forward_subsumption_resolution,[],[f20211,f13677]) ).
fof(f20466,plain,
k4_yellow_0(sK19) = k2_yellow_0(sK19,np__0),
inference(resolution,[],[f17531,f12874]) ).
fof(f20499,plain,
( ~ v2_orders_2(sK19)
| ~ v3_orders_2(sK19)
| ~ v4_orders_2(sK19)
| ~ v2_lattice3(sK19)
| ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19)
| ~ spl588_17 ),
inference(resolution,[],[f19452,f12962]) ).
fof(f20508,plain,
( ~ v3_orders_2(sK19)
| ~ v4_orders_2(sK19)
| ~ v2_lattice3(sK19)
| ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19)
| ~ spl588_17 ),
inference(forward_subsumption_resolution,[],[f20499,f12879]) ).
fof(f20509,plain,
( ~ v4_orders_2(sK19)
| ~ v2_lattice3(sK19)
| ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19)
| ~ spl588_17 ),
inference(forward_subsumption_resolution,[],[f20508,f12878]) ).
fof(f20510,plain,
( ~ v2_lattice3(sK19)
| ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19)
| ~ spl588_17 ),
inference(forward_subsumption_resolution,[],[f20509,f12877]) ).
fof(f20511,plain,
( ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19)
| ~ spl588_17 ),
inference(forward_subsumption_resolution,[],[f20510,f12875]) ).
fof(f20512,plain,
( ~ l1_orders_2(sK19)
| ~ spl588_17 ),
inference(forward_subsumption_resolution,[],[f20511,f12876]) ).
fof(f20513,plain,
( $false
| ~ spl588_17 ),
inference(forward_subsumption_resolution,[],[f20512,f12874]) ).
fof(f20514,plain,
~ spl588_17,
inference(avatar_contradiction_clause,[],[f20513]) ).
fof(f20690,plain,
! [X0] :
( m1_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f14350,f12928]) ).
fof(f21777,plain,
! [X0] :
( ~ r2_yellow_0(sK19,X0)
| v3_struct_0(sK19)
| k2_yellow_0(sK19,X0) = k1_yellow_0(k7_lattice3(sK19),X0) ),
inference(resolution,[],[f13566,f12874]) ).
fof(f21778,plain,
! [X0] :
( ~ r2_yellow_0(sK19,X0)
| k2_yellow_0(sK19,X0) = k1_yellow_0(k7_lattice3(sK19),X0) ),
inference(forward_subsumption_resolution,[],[f21777,f12880]) ).
fof(f21787,plain,
( k2_yellow_0(sK19,np__0) = k1_yellow_0(k7_lattice3(sK19),np__0)
| v3_struct_0(sK19)
| ~ v4_orders_2(sK19)
| ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19) ),
inference(resolution,[],[f21778,f17563]) ).
fof(f21795,plain,
( k2_yellow_0(sK19,np__0) = k1_yellow_0(k7_lattice3(sK19),np__0)
| ~ v4_orders_2(sK19)
| ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19) ),
inference(forward_subsumption_resolution,[],[f21787,f12880]) ).
fof(f21801,plain,
( k2_yellow_0(sK19,np__0) = k1_yellow_0(k7_lattice3(sK19),np__0)
| ~ v2_yellow_0(sK19)
| ~ l1_orders_2(sK19) ),
inference(forward_subsumption_resolution,[],[f21795,f12877]) ).
fof(f21805,plain,
( k2_yellow_0(sK19,np__0) = k1_yellow_0(k7_lattice3(sK19),np__0)
| ~ l1_orders_2(sK19) ),
inference(forward_subsumption_resolution,[],[f21801,f12876]) ).
fof(f21809,plain,
k2_yellow_0(sK19,np__0) = k1_yellow_0(k7_lattice3(sK19),np__0),
inference(forward_subsumption_resolution,[],[f21805,f12874]) ).
fof(f21813,plain,
k4_yellow_0(sK19) = k1_yellow_0(k7_lattice3(sK19),np__0),
inference(forward_demodulation,[],[f21809,f20466]) ).
fof(f22042,plain,
( v3_struct_0(sK19)
| ~ l1_orders_2(sK19)
| ~ spl588_31 ),
inference(resolution,[],[f19665,f13682]) ).
fof(f22050,plain,
( ~ l1_orders_2(sK19)
| ~ spl588_31 ),
inference(forward_subsumption_resolution,[],[f22042,f12880]) ).
fof(f22053,plain,
( $false
| ~ spl588_31 ),
inference(forward_subsumption_resolution,[],[f22050,f12874]) ).
fof(f22054,plain,
~ spl588_31,
inference(avatar_contradiction_clause,[],[f22053]) ).
fof(f23037,plain,
( v1_lattice3(k7_lattice3(sK19))
| ~ spl588_20 ),
inference(avatar_component_clause,[],[f19620]) ).
fof(f23117,plain,
( v4_orders_2(k7_lattice3(sK19))
| ~ spl588_21 ),
inference(avatar_component_clause,[],[f19623]) ).
fof(f23149,plain,
( v2_orders_2(k7_lattice3(sK19))
| ~ spl588_23 ),
inference(avatar_component_clause,[],[f19629]) ).
fof(f23934,plain,
( v3_orders_2(k7_lattice3(sK19))
| ~ spl588_22 ),
inference(avatar_component_clause,[],[f19626]) ).
fof(f41977,plain,
( ~ v3_orders_2(sK19)
| ~ v4_orders_2(sK19)
| ~ v2_orders_2(sK19)
| k7_lattice3(sK19) = g1_orders_2(u1_struct_0(k7_lattice3(sK19)),u1_orders_2(k7_lattice3(sK19))) ),
inference(resolution,[],[f20212,f12874]) ).
fof(f41983,plain,
( ~ v4_orders_2(sK19)
| ~ v2_orders_2(sK19)
| k7_lattice3(sK19) = g1_orders_2(u1_struct_0(k7_lattice3(sK19)),u1_orders_2(k7_lattice3(sK19))) ),
inference(forward_subsumption_resolution,[],[f41977,f12878]) ).
fof(f41992,plain,
( ~ v2_orders_2(sK19)
| k7_lattice3(sK19) = g1_orders_2(u1_struct_0(k7_lattice3(sK19)),u1_orders_2(k7_lattice3(sK19))) ),
inference(forward_subsumption_resolution,[],[f41983,f12877]) ).
fof(f42004,plain,
k7_lattice3(sK19) = g1_orders_2(u1_struct_0(k7_lattice3(sK19)),u1_orders_2(k7_lattice3(sK19))),
inference(forward_subsumption_resolution,[],[f41992,f12879]) ).
fof(f43006,plain,
u1_struct_0(k7_lattice3(sK19)) = k2_pre_topc(k7_lattice3(sK19)),
inference(resolution,[],[f19749,f12874]) ).
fof(f43010,plain,
( v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ spl588_24 ),
inference(superposition,[],[f19633,f43006]) ).
fof(f43016,plain,
k7_lattice3(sK19) = g1_orders_2(k2_pre_topc(k7_lattice3(sK19)),u1_orders_2(k7_lattice3(sK19))),
inference(superposition,[],[f42004,f43006]) ).
fof(f43020,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(k7_lattice3(sK19)))
| k6_waybel_0(sK19,X0) = k7_waybel_0(k7_lattice3(sK19),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| v3_struct_0(sK19)
| ~ l1_orders_2(sK19) ),
inference(superposition,[],[f18952,f43006]) ).
fof(f43030,plain,
( m1_subset_1(k3_yellow_0(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19)))
| ~ l1_orders_2(k7_lattice3(sK19)) ),
inference(superposition,[],[f13513,f43006]) ).
fof(f43091,plain,
( m1_relset_1(u1_orders_2(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19)))
| ~ l1_orders_2(k7_lattice3(sK19)) ),
inference(superposition,[],[f20690,f43006]) ).
fof(f43157,plain,
( ~ v3_struct_0(k7_lattice3(sK19))
| spl588_31 ),
inference(avatar_component_clause,[],[f19664]) ).
fof(f43216,definition,
( spl588_1109
<=> m1_relset_1(u1_orders_2(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19))) ),
introduced(definition,[new_symbols(definition,[spl588_1109])],[avatar_definition]) ).
fof(f43217,plain,
( m1_relset_1(u1_orders_2(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19)))
| ~ spl588_1109 ),
inference(avatar_component_clause,[],[f43216]) ).
fof(f43218,plain,
( ~ spl588_18
| spl588_1109 ),
inference(avatar_split_clause,[],[f43091,f43216,f19614]) ).
fof(f43297,plain,
( v1_yellow_0(k7_lattice3(sK19))
| ~ spl588_19 ),
inference(avatar_component_clause,[],[f19617]) ).
fof(f43347,definition,
( spl588_1136
<=> m1_subset_1(k3_yellow_0(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19))) ),
introduced(definition,[new_symbols(definition,[spl588_1136])],[avatar_definition]) ).
fof(f43348,plain,
( m1_subset_1(k3_yellow_0(k7_lattice3(sK19)),k2_pre_topc(k7_lattice3(sK19)))
| ~ spl588_1136 ),
inference(avatar_component_clause,[],[f43347]) ).
fof(f43349,plain,
( ~ spl588_18
| spl588_1136 ),
inference(avatar_split_clause,[],[f43030,f43347,f19614]) ).
fof(f43361,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(k7_lattice3(sK19)))
| k6_waybel_0(sK19,X0) = k7_waybel_0(k7_lattice3(sK19),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK19))
| ~ l1_orders_2(sK19) ),
inference(forward_subsumption_resolution,[],[f43020,f12880]) ).
fof(f43435,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(k7_lattice3(sK19)))
| k6_waybel_0(sK19,X0) = k7_waybel_0(k7_lattice3(sK19),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK19)) ),
inference(forward_subsumption_resolution,[],[f43361,f12874]) ).
fof(f43458,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(k7_lattice3(sK19)))
| ~ m1_subset_1(X0,k2_pre_topc(sK19))
| k6_waybel_0(sK19,X0) = k7_waybel_0(k7_lattice3(sK19),X0) ),
inference(forward_demodulation,[],[f43435,f19747]) ).
fof(f43587,plain,
( v3_struct_0(k7_lattice3(sK19))
| ~ v4_orders_2(k7_lattice3(sK19))
| u1_struct_0(k7_lattice3(sK19)) = k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19)))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19 ),
inference(resolution,[],[f43297,f13503]) ).
fof(f43593,plain,
( ~ v2_orders_2(k7_lattice3(sK19))
| ~ v3_orders_2(k7_lattice3(sK19))
| ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| v7_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19 ),
inference(resolution,[],[f43297,f17451]) ).
fof(f43594,plain,
( ~ v2_orders_2(k7_lattice3(sK19))
| ~ v3_orders_2(k7_lattice3(sK19))
| ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| v4_waybel_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19 ),
inference(resolution,[],[f43297,f17452]) ).
fof(f43595,plain,
( ~ v2_orders_2(k7_lattice3(sK19))
| ~ v3_orders_2(k7_lattice3(sK19))
| ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| m1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19 ),
inference(resolution,[],[f43297,f17453]) ).
fof(f43596,plain,
( ~ v3_orders_2(k7_lattice3(sK19))
| ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| m1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43595,f23149]) ).
fof(f43597,plain,
( ~ v3_orders_2(k7_lattice3(sK19))
| ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| v4_waybel_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43594,f23149]) ).
fof(f43598,plain,
( ~ v3_orders_2(k7_lattice3(sK19))
| ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| v7_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43593,f23149]) ).
fof(f43603,plain,
( ~ v4_orders_2(k7_lattice3(sK19))
| u1_struct_0(k7_lattice3(sK19)) = k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19)))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| spl588_31 ),
inference(forward_subsumption_resolution,[],[f43587,f43157]) ).
fof(f43605,plain,
( ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| m1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43596,f23934]) ).
fof(f43606,plain,
( ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| v4_waybel_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43597,f23934]) ).
fof(f43607,plain,
( ~ v4_orders_2(k7_lattice3(sK19))
| ~ v1_lattice3(k7_lattice3(sK19))
| v7_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43598,f23934]) ).
fof(f43612,plain,
( u1_struct_0(k7_lattice3(sK19)) = k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19)))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_21
| spl588_31 ),
inference(forward_subsumption_resolution,[],[f43603,f23117]) ).
fof(f43614,plain,
( ~ v1_lattice3(k7_lattice3(sK19))
| m1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43605,f23117]) ).
fof(f43615,plain,
( ~ v1_lattice3(k7_lattice3(sK19))
| v4_waybel_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43606,f23117]) ).
fof(f43616,plain,
( ~ v1_lattice3(k7_lattice3(sK19))
| v7_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43607,f23117]) ).
fof(f43621,plain,
( k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19))) = k2_pre_topc(k7_lattice3(sK19))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_21
| spl588_31 ),
inference(forward_demodulation,[],[f43612,f43006]) ).
fof(f43622,plain,
( m1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43614,f23037]) ).
fof(f43623,plain,
( v4_waybel_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43615,f23037]) ).
fof(f43624,plain,
( v7_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(u1_struct_0(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_subsumption_resolution,[],[f43616,f23037]) ).
fof(f43633,definition,
( spl588_1166
<=> k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19))) = k2_pre_topc(k7_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl588_1166])],[avatar_definition]) ).
fof(f43634,plain,
( k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19))) = k2_pre_topc(k7_lattice3(sK19))
| ~ spl588_1166 ),
inference(avatar_component_clause,[],[f43633]) ).
fof(f43635,plain,
( ~ spl588_18
| spl588_1166
| ~ spl588_19
| ~ spl588_21
| spl588_31 ),
inference(avatar_split_clause,[],[f43621,f19664,f19623,f19617,f43633,f19614]) ).
fof(f43636,plain,
( m1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_demodulation,[],[f43622,f43006]) ).
fof(f43637,plain,
( v4_waybel_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_demodulation,[],[f43623,f43006]) ).
fof(f43638,plain,
( v7_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK19))),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_demodulation,[],[f43624,f43006]) ).
fof(f43645,plain,
( m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_demodulation,[],[f43636,f19557]) ).
fof(f43646,plain,
( v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_demodulation,[],[f43637,f19557]) ).
fof(f43647,plain,
( v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ l1_orders_2(k7_lattice3(sK19))
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(forward_demodulation,[],[f43638,f19557]) ).
fof(f43650,definition,
( spl588_1168
<=> v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19))))) ),
introduced(definition,[new_symbols(definition,[spl588_1168])],[avatar_definition]) ).
fof(f43651,plain,
( v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ spl588_1168 ),
inference(avatar_component_clause,[],[f43650]) ).
fof(f43652,plain,
( ~ spl588_18
| spl588_1168
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(avatar_split_clause,[],[f43646,f19629,f19626,f19623,f19620,f19617,f43650,f19614]) ).
fof(f43654,definition,
( spl588_1169
<=> v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19))))) ),
introduced(definition,[new_symbols(definition,[spl588_1169])],[avatar_definition]) ).
fof(f43655,plain,
( v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ spl588_1169 ),
inference(avatar_component_clause,[],[f43654]) ).
fof(f43656,plain,
( ~ spl588_18
| spl588_1169
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(avatar_split_clause,[],[f43647,f19629,f19626,f19623,f19620,f19617,f43654,f19614]) ).
fof(f43667,definition,
( spl588_1170
<=> m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19))))) ),
introduced(definition,[new_symbols(definition,[spl588_1170])],[avatar_definition]) ).
fof(f43668,plain,
( m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(k7_lattice3(sK19)))))
| ~ spl588_1170 ),
inference(avatar_component_clause,[],[f43667]) ).
fof(f43669,plain,
( ~ spl588_18
| spl588_1170
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23 ),
inference(avatar_split_clause,[],[f43645,f19629,f19626,f19623,f19620,f19617,f43667,f19614]) ).
fof(f44013,plain,
( l1_orders_2(g1_orders_2(k2_pre_topc(k7_lattice3(sK19)),u1_orders_2(k7_lattice3(sK19))))
| ~ spl588_1109 ),
inference(resolution,[],[f43217,f15879]) ).
fof(f44018,plain,
( l1_orders_2(k7_lattice3(sK19))
| ~ spl588_1109 ),
inference(forward_demodulation,[],[f44013,f43016]) ).
fof(f44071,plain,
( k1_yellow_0(k7_lattice3(sK19),np__0) = k3_yellow_0(k7_lattice3(sK19))
| ~ spl588_1109 ),
inference(resolution,[],[f44018,f17529]) ).
fof(f44165,plain,
( k4_yellow_0(sK19) = k3_yellow_0(k7_lattice3(sK19))
| ~ spl588_1109 ),
inference(forward_demodulation,[],[f44071,f21813]) ).
fof(f44317,plain,
( k2_pre_topc(k7_lattice3(sK19)) = k7_waybel_0(k7_lattice3(sK19),k4_yellow_0(sK19))
| ~ spl588_1109
| ~ spl588_1166 ),
inference(superposition,[],[f43634,f44165]) ).
fof(f52983,plain,
( ~ m1_subset_1(k3_yellow_0(k7_lattice3(sK19)),k2_pre_topc(sK19))
| k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19))) = k6_waybel_0(sK19,k3_yellow_0(k7_lattice3(sK19)))
| ~ spl588_1136 ),
inference(resolution,[],[f43458,f43348]) ).
fof(f52986,plain,
( ~ m1_subset_1(k4_yellow_0(sK19),k2_pre_topc(sK19))
| k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19))) = k6_waybel_0(sK19,k3_yellow_0(k7_lattice3(sK19)))
| ~ spl588_1109
| ~ spl588_1136 ),
inference(forward_demodulation,[],[f52983,f44165]) ).
fof(f52987,plain,
( k7_waybel_0(k7_lattice3(sK19),k3_yellow_0(k7_lattice3(sK19))) = k6_waybel_0(sK19,k3_yellow_0(k7_lattice3(sK19)))
| ~ spl588_1109
| ~ spl588_1136 ),
inference(forward_subsumption_resolution,[],[f52986,f20192]) ).
fof(f52988,plain,
( k6_waybel_0(sK19,k4_yellow_0(sK19)) = k7_waybel_0(k7_lattice3(sK19),k4_yellow_0(sK19))
| ~ spl588_1109
| ~ spl588_1136 ),
inference(forward_demodulation,[],[f52987,f44165]) ).
fof(f52989,plain,
( k6_waybel_0(sK19,k4_yellow_0(sK19)) = k2_pre_topc(k7_lattice3(sK19))
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166 ),
inference(forward_demodulation,[],[f52988,f44317]) ).
fof(f52990,plain,
( u1_struct_0(sK19) = k2_pre_topc(k7_lattice3(sK19))
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166 ),
inference(forward_demodulation,[],[f52989,f19693]) ).
fof(f52991,plain,
( k2_pre_topc(sK19) = k2_pre_topc(k7_lattice3(sK19))
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166 ),
inference(forward_demodulation,[],[f52990,f19747]) ).
fof(f52992,plain,
( v4_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(sK19))))
| ~ spl588_24
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166 ),
inference(superposition,[],[f43010,f52991]) ).
fof(f53001,plain,
( v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(sK19))))
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1168 ),
inference(superposition,[],[f43651,f52991]) ).
fof(f53002,plain,
( v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(sK19))))
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1169 ),
inference(superposition,[],[f43655,f52991]) ).
fof(f53003,plain,
( m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(sK19))))
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1170 ),
inference(superposition,[],[f43668,f52991]) ).
fof(f53018,plain,
( $false
| spl588_16
| ~ spl588_24
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166 ),
inference(forward_subsumption_resolution,[],[f52992,f19750]) ).
fof(f53019,plain,
( spl588_16
| ~ spl588_24
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166 ),
inference(avatar_contradiction_clause,[],[f53018]) ).
fof(f53020,plain,
( ~ m1_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(sK19))))
| spl588_13 ),
inference(forward_demodulation,[],[f19440,f19747]) ).
fof(f53021,plain,
( $false
| spl588_13
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1170 ),
inference(forward_subsumption_resolution,[],[f53020,f53003]) ).
fof(f53022,plain,
( spl588_13
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1170 ),
inference(avatar_contradiction_clause,[],[f53021]) ).
fof(f53023,plain,
( ~ v4_waybel_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(sK19))))
| spl588_14 ),
inference(forward_demodulation,[],[f19443,f19747]) ).
fof(f53024,plain,
( $false
| spl588_14
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1168 ),
inference(forward_subsumption_resolution,[],[f53023,f53001]) ).
fof(f53025,plain,
( spl588_14
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1168 ),
inference(avatar_contradiction_clause,[],[f53024]) ).
fof(f53026,plain,
( ~ v7_yellow_0(k2_yellow_1(k9_waybel_0(sK19)),k2_yellow_1(k1_zfmisc_1(k2_pre_topc(sK19))))
| spl588_15 ),
inference(forward_demodulation,[],[f19446,f19747]) ).
fof(f53027,plain,
( $false
| spl588_15
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1169 ),
inference(forward_subsumption_resolution,[],[f53026,f53002]) ).
fof(f53028,plain,
( spl588_15
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1169 ),
inference(avatar_contradiction_clause,[],[f53027]) ).
cnf(s9,plain,
( ~ spl588_13
| ~ spl588_14
| ~ spl588_15
| ~ spl588_16
| spl588_17 ),
inference(sat_conversion,[],[f19453]) ).
cnf(s14,plain,
( ~ spl588_18
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23
| spl588_24 ),
inference(sat_conversion,[],[f19634]) ).
cnf(s25,plain,
spl588_18,
inference(sat_conversion,[],[f19728]) ).
cnf(s27,plain,
spl588_22,
inference(sat_conversion,[],[f19734]) ).
cnf(s29,plain,
spl588_23,
inference(sat_conversion,[],[f19740]) ).
cnf(s31,plain,
spl588_21,
inference(sat_conversion,[],[f19746]) ).
cnf(s45,plain,
spl588_20,
inference(sat_conversion,[],[f20070]) ).
cnf(s47,plain,
spl588_19,
inference(sat_conversion,[],[f20076]) ).
cnf(s83,plain,
~ spl588_17,
inference(sat_conversion,[],[f20514]) ).
cnf(s143,plain,
~ spl588_31,
inference(sat_conversion,[],[f22054]) ).
cnf(s1099,plain,
( ~ spl588_18
| spl588_1109 ),
inference(sat_conversion,[],[f43218]) ).
cnf(s1126,plain,
( ~ spl588_18
| spl588_1136 ),
inference(sat_conversion,[],[f43349]) ).
cnf(s1162,plain,
( ~ spl588_18
| ~ spl588_19
| ~ spl588_21
| spl588_31
| spl588_1166 ),
inference(sat_conversion,[],[f43635]) ).
cnf(s1164,plain,
( ~ spl588_18
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23
| spl588_1168 ),
inference(sat_conversion,[],[f43652]) ).
cnf(s1165,plain,
( ~ spl588_18
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23
| spl588_1169 ),
inference(sat_conversion,[],[f43656]) ).
cnf(s1167,plain,
( ~ spl588_18
| ~ spl588_19
| ~ spl588_20
| ~ spl588_21
| ~ spl588_22
| ~ spl588_23
| spl588_1170 ),
inference(sat_conversion,[],[f43669]) ).
cnf(s1742,plain,
( spl588_16
| ~ spl588_24
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166 ),
inference(sat_conversion,[],[f53019]) ).
cnf(s1743,plain,
( spl588_13
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1170 ),
inference(sat_conversion,[],[f53022]) ).
cnf(s1744,plain,
( spl588_14
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1168 ),
inference(sat_conversion,[],[f53025]) ).
cnf(s1745,plain,
( spl588_15
| ~ spl588_1109
| ~ spl588_1136
| ~ spl588_1166
| ~ spl588_1169 ),
inference(sat_conversion,[],[f53028]) ).
cnf(s2135,plain,
spl588_1170,
inference(rat,[],[s1167,s27,s29,s31,s45,s47,s25]) ).
cnf(s2137,plain,
spl588_1169,
inference(rat,[],[s1165,s27,s29,s31,s45,s47,s25]) ).
cnf(s2138,plain,
spl588_1168,
inference(rat,[],[s1164,s27,s29,s31,s45,s47,s25]) ).
cnf(s2140,plain,
spl588_1166,
inference(rat,[],[s1162,s31,s143,s47,s25]) ).
cnf(s2160,plain,
spl588_1136,
inference(rat,[],[s1126,s25]) ).
cnf(s2184,plain,
spl588_1109,
inference(rat,[],[s1099,s25]) ).
cnf(s2216,plain,
spl588_15,
inference(rat,[],[s1745,s2137,s2140,s2160,s2184]) ).
cnf(s2217,plain,
spl588_14,
inference(rat,[],[s1744,s2138,s2140,s2160,s2184]) ).
cnf(s2218,plain,
spl588_13,
inference(rat,[],[s1743,s2135,s2140,s2160,s2184]) ).
cnf(s2441,plain,
spl588_24,
inference(rat,[],[s14,s29,s27,s31,s45,s47,s25]) ).
cnf(s2442,plain,
spl588_16,
inference(rat,[],[s1742,s2140,s2160,s2184,s2441]) ).
cnf(s2444,plain,
$false,
inference(rat,[],[s9,s83,s2442,s2216,s2217,s2218]) ).
fof(f53029,plain,
$false,
inference(avatar_sat_refutation,[],[s2444]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT348+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.41 % Computer : n014.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 14:53:17 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.44 Running first-order theorem proving
% 0.15/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.96/3.44 % (902120)Detected formulas, will run a generic FOF schedule.
% 16.96/3.44 % (902131)dis-21_1_sil=8000:lcm=predicate:random_seed=3240860588:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 16.96/3.44 % (902125)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2146020973:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 16.96/3.44 % (902131)Instruction limit reached!
% 16.96/3.44 % (902131)------------------------------
% 16.96/3.44 % (902131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.96/3.44 % (902131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.96/3.44 % (902131)CaDiCaL version: 2.1.3
% 16.96/3.44 % (902131)Termination reason: Instruction limit
% 16.96/3.44 % (902131)Termination phase: Preprocessing 2
% 16.96/3.44 % (902131)Time elapsed: 0.066 s
% 16.96/3.44 % (902131)Peak memory usage: 98 MB
% 16.96/3.44 % (902131)Instructions burned: 129 (million)
% 16.96/3.44 % (902129)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3446562563:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 16.96/3.44 % (902126)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3064557264:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 16.96/3.44 % (902128)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3823104700:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 16.96/3.44 % (902127)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=923762650:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 16.96/3.44 % (902130)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=248274206:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 16.96/3.44 % (902134)lrs+10_1_sil=8000:sp=occurrence:random_seed=3984596826:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 16.96/3.44 % (902128)Refutation not found, incomplete strategy
% 16.96/3.44 % (902128)------------------------------
% 16.96/3.44 % (902128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.96/3.44 % (902128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.96/3.44 % (902128)CaDiCaL version: 2.1.3
% 16.96/3.44 % (902128)Termination reason: Refutation not found, incomplete strategy
% 16.96/3.44 % (902128)Time elapsed: 0.076 s
% 16.96/3.44 % (902128)Peak memory usage: 100 MB
% 16.96/3.44 % (902128)Instructions burned: 65 (million)
% 16.96/3.44 % (902129)Instruction limit reached!
% 16.96/3.44 % (902129)------------------------------
% 16.96/3.44 % (902129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.96/3.44 % (902129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.96/3.44 % (902129)CaDiCaL version: 2.1.3
% 16.96/3.44 % (902129)Termination reason: Instruction limit
% 16.96/3.44 % (902129)Termination phase: Property scanning
% 16.96/3.44 % (902129)Time elapsed: 0.142 s
% 16.96/3.44 % (902129)Peak memory usage: 100 MB
% 16.96/3.44 % (902129)Instructions burned: 119 (million)
% 16.96/3.44 % (902130)Instruction limit reached!
% 16.96/3.45 % (902130)------------------------------
% 16.96/3.45 % (902130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.96/3.45 % (902130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.96/3.45 % (902130)CaDiCaL version: 2.1.3
% 16.96/3.45 % (902130)Termination reason: Instruction limit
% 16.96/3.45 % (902130)Termination phase: SInE selection
% 16.96/3.45 % (902130)Time elapsed: 0.126 s
% 16.96/3.45 % (902130)Peak memory usage: 96 MB
% 16.96/3.45 % (902130)Instructions burned: 139 (million)
% 16.96/3.45 % (902134)Instruction limit reached!
% 16.96/3.45 % (902134)------------------------------
% 16.96/3.45 % (902134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.96/3.45 % (902134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.96/3.45 % (902134)CaDiCaL version: 2.1.3
% 16.96/3.45 % (902134)Termination reason: Instruction limit
% 16.96/3.45 % (902134)Termination phase: Saturation
% 16.96/3.45 % (902134)Time elapsed: 0.108 s
% 16.96/3.45 % (902134)Peak memory usage: 104 MB
% 16.96/3.45 % (902134)Instructions burned: 287 (million)
% 16.96/3.45 % (902141)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2619458930:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 24.56/4.43 % (902143)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=354883675:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 24.56/4.43 % (902141)Instruction limit reached!
% 24.56/4.43 % (902141)------------------------------
% 24.56/4.43 % (902141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.56/4.43 % (902141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.56/4.43 % (902141)CaDiCaL version: 2.1.3
% 24.56/4.43 % (902141)Termination reason: Instruction limit
% 24.56/4.43 % (902141)Termination phase: Preprocessing 3
% 24.56/4.43 % (902141)Time elapsed: 0.091 s
% 24.56/4.43 % (902141)Peak memory usage: 98 MB
% 24.56/4.43 % (902141)Instructions burned: 158 (million)
% 24.56/4.43 % (902143)Instruction limit reached!
% 24.56/4.43 % (902143)------------------------------
% 24.56/4.43 % (902143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.56/4.43 % (902143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.56/4.43 % (902143)CaDiCaL version: 2.1.3
% 24.56/4.43 % (902143)Termination reason: Instruction limit
% 24.56/4.43 % (902143)Termination phase: Unused predicate definition removal
% 24.56/4.43 % (902143)Time elapsed: 0.086 s
% 24.56/4.43 % (902143)Peak memory usage: 99 MB
% 24.56/4.43 % (902143)Instructions burned: 248 (million)
% 24.56/4.43 % (902142)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3185147342:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 24.56/4.43 % (902128)------------------------------
% 24.56/4.43 % (902128)------------------------------
% 24.56/4.43 % (902147)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1574809700:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 24.56/4.43 % (902146)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1963647436:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 24.56/4.43 % (902142)Instruction limit reached!
% 24.56/4.43 % (902142)------------------------------
% 24.56/4.43 % (902142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.56/4.43 % (902142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.56/4.43 % (902142)CaDiCaL version: 2.1.3
% 24.56/4.43 % (902142)Termination reason: Instruction limit
% 24.56/4.43 % (902142)Termination phase: Saturation
% 24.56/4.43 % (902142)Time elapsed: 0.292 s
% 24.56/4.43 % (902142)Peak memory usage: 102 MB
% 24.56/4.43 % (902142)Instructions burned: 325 (million)
% 24.56/4.43 % (902149)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2852193258:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 24.56/4.43 % (902149)Instruction limit reached!
% 24.56/4.43 % (902149)------------------------------
% 24.56/4.43 % (902149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.56/4.43 % (902149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.56/4.43 % (902149)CaDiCaL version: 2.1.3
% 24.56/4.43 % (902149)Termination reason: Instruction limit
% 24.56/4.43 % (902149)Termination phase: Preprocessing 3
% 24.56/4.43 % (902149)Time elapsed: 0.138 s
% 24.56/4.43 % (902149)Peak memory usage: 100 MB
% 24.56/4.43 % (902149)Instructions burned: 113 (million)
% 24.56/4.43 % (902146)Instruction limit reached!
% 24.56/4.43 % (902146)------------------------------
% 24.56/4.43 % (902146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.56/4.43 % (902146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.56/4.43 % (902146)CaDiCaL version: 2.1.3
% 24.56/4.43 % (902146)Termination reason: Instruction limit
% 24.56/4.43 % (902146)Termination phase: Saturation
% 24.56/4.43 % (902146)Time elapsed: 0.293 s
% 24.56/4.43 % (902146)Peak memory usage: 104 MB
% 24.56/4.43 % (902146)Instructions burned: 295 (million)
% 24.56/4.43 % (902152)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2126501:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 24.56/4.43 % (902155)lrs+10_1_sil=8000:sp=occurrence:random_seed=129291150:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 24.56/4.43 % (902154)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4268892334:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 24.56/4.43 % (902152)Instruction limit reached!
% 21.81/7.18 % (902152)------------------------------
% 21.81/7.18 % (902152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902152)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902152)Termination reason: Instruction limit
% 21.81/7.18 % (902152)Termination phase: Naming
% 21.81/7.18 % (902152)Time elapsed: 0.160 s
% 21.81/7.18 % (902152)Peak memory usage: 105 MB
% 21.81/7.18 % (902152)Instructions burned: 128 (million)
% 21.81/7.18 % (902154)Instruction limit reached!
% 21.81/7.18 % (902154)------------------------------
% 21.81/7.18 % (902154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902154)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902154)Termination reason: Instruction limit
% 21.81/7.18 % (902154)Termination phase: Initialization
% 21.81/7.18 % (902154)Time elapsed: 0.097 s
% 21.81/7.18 % (902154)Peak memory usage: 96 MB
% 21.81/7.18 % (902154)Instructions burned: 114 (million)
% 21.81/7.18 % (902160)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1852095654:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 21.81/7.18 % (902159)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1531999820:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 21.81/7.18 % (902155)Instruction limit reached!
% 21.81/7.18 % (902155)------------------------------
% 21.81/7.18 % (902155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902155)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902155)Termination reason: Instruction limit
% 21.81/7.18 % (902155)Termination phase: Saturation
% 21.81/7.18 % (902155)Time elapsed: 0.539 s
% 21.81/7.18 % (902155)Peak memory usage: 114 MB
% 21.81/7.18 % (902155)Instructions burned: 907 (million)
% 21.81/7.18 % (902147)Instruction limit reached!
% 21.81/7.18 % (902147)------------------------------
% 21.81/7.18 % (902147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902147)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902147)Termination reason: Instruction limit
% 21.81/7.18 % (902147)Termination phase: Saturation
% 21.81/7.18 % (902147)Time elapsed: 1.240 s
% 21.81/7.18 % (902147)Peak memory usage: 318 MB
% 21.81/7.18 % (902147)Instructions burned: 2351 (million)
% 21.81/7.18 % (902163)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1690163401:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 21.81/7.18 % (902159)Instruction limit reached!
% 21.81/7.18 % (902159)------------------------------
% 21.81/7.18 % (902159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902159)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902159)Termination reason: Instruction limit
% 21.81/7.18 % (902159)Termination phase: Saturation
% 21.81/7.18 % (902159)Time elapsed: 0.465 s
% 21.81/7.18 % (902159)Peak memory usage: 102 MB
% 21.81/7.18 % (902159)Instructions burned: 437 (million)
% 21.81/7.18 % (902164)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3212016184:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 21.81/7.18 % (902163)Instruction limit reached!
% 21.81/7.18 % (902163)------------------------------
% 21.81/7.18 % (902163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902163)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902163)Termination reason: Instruction limit
% 21.81/7.18 % (902163)Termination phase: Saturation
% 21.81/7.18 % (902163)Time elapsed: 0.143 s
% 21.81/7.18 % (902163)Peak memory usage: 101 MB
% 21.81/7.18 % (902163)Instructions burned: 135 (million)
% 21.81/7.18 % (902166)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2685924759:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 21.81/7.18 % (902168)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2063318112:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/125Mi)
% 21.81/7.18 % (902164)Instruction limit reached!
% 21.81/7.18 % (902164)------------------------------
% 21.81/7.18 % (902164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902164)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902164)Termination reason: Instruction limit
% 21.81/7.18 % (902164)Termination phase: Property scanning
% 21.81/7.18 % (902164)Time elapsed: 0.243 s
% 21.81/7.18 % (902164)Peak memory usage: 112 MB
% 21.81/7.18 % (902164)Instructions burned: 598 (million)
% 21.81/7.18 % (902168)Instruction limit reached!
% 21.81/7.18 % (902168)------------------------------
% 21.81/7.18 % (902168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902168)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902168)Termination reason: Instruction limit
% 21.81/7.18 % (902168)Termination phase: SInE selection
% 21.81/7.18 % (902168)Time elapsed: 0.060 s
% 21.81/7.18 % (902168)Peak memory usage: 96 MB
% 21.81/7.18 % (902168)Instructions burned: 125 (million)
% 21.81/7.18 % (902171)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2663514663:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 21.81/7.18 % (902172)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1718484638:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 21.81/7.18 % (902172)Refutation not found, incomplete strategy
% 21.81/7.18 % (902172)------------------------------
% 21.81/7.18 % (902172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902172)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902172)Termination reason: Refutation not found, incomplete strategy
% 21.81/7.18 % (902172)Time elapsed: 0.051 s
% 21.81/7.18 % (902172)Peak memory usage: 100 MB
% 21.81/7.18 % (902172)Instructions burned: 61 (million)
% 21.81/7.18 % (902171)Instruction limit reached!
% 21.81/7.18 % (902171)------------------------------
% 21.81/7.18 % (902171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902171)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902171)Termination reason: Instruction limit
% 21.81/7.18 % (902171)Termination phase: Initialization
% 21.81/7.18 % (902171)Time elapsed: 0.065 s
% 21.81/7.18 % (902171)Peak memory usage: 96 MB
% 21.81/7.18 % (902171)Instructions burned: 135 (million)
% 21.81/7.18 % (902175)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=332476410:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2969 on theBenchmark for (2969ds/431Mi)
% 21.81/7.18 % (902172)------------------------------
% 21.81/7.18 % (902172)------------------------------
% 21.81/7.18 % (902177)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3593260296:i=6060:aac=none:ins=25_2967 on theBenchmark for (2967ds/6060Mi)
% 21.81/7.18 % (902175)Instruction limit reached!
% 21.81/7.18 % (902175)------------------------------
% 21.81/7.18 % (902175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902175)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902175)Termination reason: Instruction limit
% 21.81/7.18 % (902175)Termination phase: Saturation
% 21.81/7.18 % (902175)Time elapsed: 0.258 s
% 21.81/7.18 % (902175)Peak memory usage: 105 MB
% 21.81/7.18 % (902175)Instructions burned: 431 (million)
% 21.81/7.18 % (902179)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=892403105:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 21.81/7.18 % (902179)Instruction limit reached!
% 21.81/7.18 % (902179)------------------------------
% 21.81/7.18 % (902179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902179)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902179)Termination reason: Instruction limit
% 21.81/7.18 % (902179)Termination phase: Preprocessing 2
% 21.81/7.18 % (902179)Time elapsed: 0.089 s
% 21.81/7.18 % (902179)Peak memory usage: 103 MB
% 21.81/7.18 % (902179)Instructions burned: 151 (million)
% 21.81/7.18 % (902181)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=250119664:i=14155:bd=all_2962 on theBenchmark for (2962ds/14155Mi)
% 21.81/7.18 % (902160)Instruction limit reached!
% 21.81/7.18 % (902160)------------------------------
% 21.81/7.18 % (902160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902160)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902160)Termination reason: Instruction limit
% 21.81/7.18 % (902160)Termination phase: Saturation
% 21.81/7.18 % (902160)Time elapsed: 3.406 s
% 21.81/7.18 % (902160)Peak memory usage: 189 MB
% 21.81/7.18 % (902160)Instructions burned: 5202 (million)
% 21.81/7.18 % (902183)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3930183234:i=667:av=off:fsr=off_2946 on theBenchmark for (2946ds/667Mi)
% 21.81/7.18 % (902183)Instruction limit reached!
% 21.81/7.18 % (902183)------------------------------
% 21.81/7.18 % (902183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902183)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902183)Termination reason: Instruction limit
% 21.81/7.18 % (902183)Termination phase: Property scanning
% 21.81/7.18 % (902183)Time elapsed: 0.434 s
% 21.81/7.18 % (902183)Peak memory usage: 120 MB
% 21.81/7.18 % (902183)Instructions burned: 668 (million)
% 21.81/7.18 % (902185)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1426115376:s2a=on:i=185:s2at=1.8:fdi=4_2940 on theBenchmark for (2940ds/185Mi)
% 21.81/7.18 % (902126)First to succeed.
% 21.81/7.18 % (902126)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-902120"
% 21.81/7.18 % (902185)Instruction limit reached!
% 21.81/7.18 % (902185)------------------------------
% 21.81/7.18 % (902185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/7.18 % (902185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/7.18 % (902185)CaDiCaL version: 2.1.3
% 21.81/7.18 % (902185)Termination reason: Instruction limit
% 21.81/7.18 % (902185)Termination phase: NewCNF
% 21.81/7.18 % (902185)Time elapsed: 0.151 s
% 21.81/7.18 % (902185)Peak memory usage: 105 MB
% 21.81/7.18 % (902185)Instructions burned: 185 (million)
% 21.81/7.18 % (902126)Refutation found. Thanks to Tanya!
% 21.81/7.18 % SZS status Theorem for theBenchmark
% 21.81/7.18 % SZS output start Proof for theBenchmark
% See solution above
% 44.46/7.38 % (902126)------------------------------
% 44.46/7.38 % (902126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.46/7.38 % (902126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.46/7.38 % (902126)CaDiCaL version: 2.1.3
% 44.46/7.38 % (902126)Termination reason: Refutation
% 44.46/7.38 % (902126)Time elapsed: 5.747 s
% 44.46/7.38 % (902126)Peak memory usage: 237 MB
% 44.46/7.38 % (902126)Instructions burned: 10913 (million)
% 44.46/7.38 % (902126)------------------------------
% 44.46/7.38 % (902126)------------------------------
% 44.46/7.38 % (902120)Success in time 6.483 s
% 44.46/7.38 % Vampire exiting
%------------------------------------------------------------------------------