%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU410+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 12:48:47 PM UTC 2026
% Result : Theorem 46.94s 16.07s
% Output : Refutation 101.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 38
% Syntax : Number of formulae : 484 ( 64 unt; 18 def)
% Number of atoms : 3057 ( 134 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 4677 (2104 ~;2202 |; 260 &)
% ( 42 <=>; 69 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 19 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 6 con; 0-4 aty)
% Number of variables : 658 ( 0 sgn 628 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f31,axiom,
! [X0,X1,X2] :
( X2 = k3_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f7737,axiom,
! [X0] :
( ( v4_orders_2(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( r1_orders_2(X0,X1,X2)
& r1_orders_2(X0,X2,X1) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_orders_2) ).
fof(f11560,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f11645,axiom,
! [X0,X1,X2] :
( ( v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k13_lattice3) ).
fof(f11646,axiom,
! [X0,X1,X2] :
( ( v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k13_lattice3(X0,X1,X2) = k13_lattice3(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k13_lattice3) ).
fof(f14804,axiom,
! [X0] :
( ( v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( X3 = k13_lattice3(X0,X1,X2)
<=> ( r1_orders_2(X0,X1,X3)
& r1_orders_2(X0,X2,X3)
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> ( ( r1_orders_2(X0,X1,X4)
& r1_orders_2(X0,X2,X4) )
=> r1_orders_2(X0,X3,X4) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t22_yellow_0) ).
fof(f14806,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( X1 = k13_lattice3(X0,X1,X2)
<=> r1_orders_2(X0,X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_yellow_0) ).
fof(f14960,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v12_waybel_0(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r1_orders_2(X0,X3,X2) )
=> r2_hidden(X3,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d19_waybel_0) ).
fof(f14961,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v13_waybel_0(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r1_orders_2(X0,X2,X3) )
=> r2_hidden(X3,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d20_waybel_0) ).
fof(f14979,axiom,
! [X0] :
( ( v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v12_waybel_0(X1,X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( v1_waybel_0(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
=> r2_hidden(k13_lattice3(X0,X2,X3),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_waybel_0) ).
fof(f15247,axiom,
! [X0] :
( ( v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r1_orders_2(X0,X1,X2)
=> r1_orders_2(X0,k13_lattice3(X0,X1,X3),k13_lattice3(X0,X2,X3)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_waybel_1) ).
fof(f15906,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k13_lattice3(X0,X1,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_yellow_5) ).
fof(f15908,axiom,
! [X0] :
( ( v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r1_orders_2(X0,k13_lattice3(X0,X1,X2),X3)
=> r1_orders_2(X0,X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_yellow_5) ).
fof(f16349,axiom,
! [X0] : u1_struct_0(k3_yellow_1(X0)) = k1_zfmisc_1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_waybel_7) ).
fof(f16826,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v1_xboole_0(u1_struct_0(X0))
& v1_waybel_0(u1_struct_0(X0),X0)
& v12_waybel_0(u1_struct_0(X0),X0)
& m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_waybel13) ).
fof(f19041,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(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(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X2 = X4
& X3 = X5
& r1_latsum_1(X0,X1)
& v3_orders_2(X0)
& v3_orders_2(X1) )
=> ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(X1,X4,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_latsum_1) ).
fof(f19045,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& l1_orders_2(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(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( v1_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& v12_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& r1_latsum_1(X0,X1)
& X2 = X4
& X3 = X5 )
=> k13_lattice3(X0,X2,X3) = k13_lattice3(X1,X4,X5) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_latsum_1) ).
fof(f19046,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& l1_orders_2(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(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( v1_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& v12_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& r1_latsum_1(X0,X1)
& X2 = X4
& X3 = X5 )
=> k13_lattice3(X0,X2,X3) = k13_lattice3(X1,X4,X5) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f19045]) ).
fof(f19088,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( k13_lattice3(X0,X2,X3) != k13_lattice3(X1,X4,X5)
& v1_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& v12_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& r1_latsum_1(X0,X1)
& X2 = X4
& X3 = X5
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(X1)) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& l1_orders_2(X1) )
& ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f19046]) ).
fof(f19089,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( k13_lattice3(X0,X2,X3) != k13_lattice3(X1,X4,X5)
& v1_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& v12_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& r1_latsum_1(X0,X1)
& X2 = X4
& X3 = X5
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(X1)) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& l1_orders_2(X1) )
& ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f19088]) ).
fof(f19127,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11560]) ).
fof(f19128,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19127]) ).
fof(f19131,plain,
! [X0] :
( ( ~ v1_xboole_0(u1_struct_0(X0))
& v1_waybel_0(u1_struct_0(X0),X0)
& v12_waybel_0(u1_struct_0(X0),X0)
& m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16826]) ).
fof(f19132,plain,
! [X0] :
( ( ~ v1_xboole_0(u1_struct_0(X0))
& v1_waybel_0(u1_struct_0(X0),X0)
& v12_waybel_0(u1_struct_0(X0),X0)
& m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19131]) ).
fof(f19149,plain,
! [X0] :
( ! [X1] :
( ( v12_waybel_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| ~ r1_orders_2(X0,X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14960]) ).
fof(f19150,plain,
! [X0] :
( ! [X1] :
( ( v12_waybel_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| ~ r1_orders_2(X0,X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19149]) ).
fof(f19162,plain,
! [X0] :
( ! [X1] :
( ( v13_waybel_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| ~ r1_orders_2(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14961]) ).
fof(f19163,plain,
! [X0] :
( ! [X1] :
( ( v13_waybel_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| ~ r1_orders_2(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19162]) ).
fof(f19164,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(X1,X4,X5) )
| X2 != X4
| X3 != X5
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f19041]) ).
fof(f19165,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(X1,X4,X5) )
| X2 != X4
| X3 != X5
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19164]) ).
fof(f19198,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( r1_orders_2(X0,X1,X3)
| ~ r1_orders_2(X0,k13_lattice3(X0,X1,X2),X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15908]) ).
fof(f19199,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( r1_orders_2(X0,X1,X3)
| ~ r1_orders_2(X0,k13_lattice3(X0,X1,X2),X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19198]) ).
fof(f19200,plain,
! [X0] :
( ! [X1] :
( k13_lattice3(X0,X1,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15906]) ).
fof(f19201,plain,
! [X0] :
( ! [X1] :
( k13_lattice3(X0,X1,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19200]) ).
fof(f19206,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( r1_orders_2(X0,k13_lattice3(X0,X1,X3),k13_lattice3(X0,X2,X3))
| ~ r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15247]) ).
fof(f19207,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( r1_orders_2(X0,k13_lattice3(X0,X1,X3),k13_lattice3(X0,X2,X3))
| ~ r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19206]) ).
fof(f19209,plain,
! [X0] :
( ! [X1] :
( ( v1_waybel_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( r2_hidden(k13_lattice3(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14979]) ).
fof(f19210,plain,
! [X0] :
( ! [X1] :
( ( v1_waybel_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( r2_hidden(k13_lattice3(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19209]) ).
fof(f19211,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k13_lattice3(X0,X1,X2)
<=> r1_orders_2(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14806]) ).
fof(f19212,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k13_lattice3(X0,X1,X2)
<=> r1_orders_2(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19211]) ).
fof(f19213,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k13_lattice3(X0,X1,X2)
<=> ( r1_orders_2(X0,X1,X3)
& r1_orders_2(X0,X2,X3)
& ! [X4] :
( r1_orders_2(X0,X3,X4)
| ~ r1_orders_2(X0,X1,X4)
| ~ r1_orders_2(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14804]) ).
fof(f19214,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k13_lattice3(X0,X1,X2)
<=> ( r1_orders_2(X0,X1,X3)
& r1_orders_2(X0,X2,X3)
& ! [X4] :
( r1_orders_2(X0,X3,X4)
| ~ r1_orders_2(X0,X1,X4)
| ~ r1_orders_2(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19213]) ).
fof(f19215,plain,
! [X0,X1,X2] :
( k13_lattice3(X0,X1,X2) = k13_lattice3(X0,X2,X1)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f11646]) ).
fof(f19216,plain,
! [X0,X1,X2] :
( k13_lattice3(X0,X1,X2) = k13_lattice3(X0,X2,X1)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f19215]) ).
fof(f19217,plain,
! [X0,X1,X2] :
( m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f11645]) ).
fof(f19218,plain,
! [X0,X1,X2] :
( m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f19217]) ).
fof(f19227,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f678]) ).
fof(f19228,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f19227]) ).
fof(f19538,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f19674,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ r1_orders_2(X0,X1,X2)
| ~ r1_orders_2(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7737]) ).
fof(f19675,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ r1_orders_2(X0,X1,X2)
| ~ r1_orders_2(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19674]) ).
fof(f20177,plain,
( k13_lattice3(sK22,sK24,sK25) != k13_lattice3(sK23,sK26,sK27)
& v1_waybel_0(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),sK23)
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),sK23)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),k1_zfmisc_1(u1_struct_0(sK23)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),sK22)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),k1_zfmisc_1(u1_struct_0(sK22)))
& r1_latsum_1(sK22,sK23)
& sK24 = sK26
& sK25 = sK27
& m1_subset_1(sK27,u1_struct_0(sK23))
& m1_subset_1(sK26,u1_struct_0(sK23))
& m1_subset_1(sK25,u1_struct_0(sK22))
& m1_subset_1(sK24,u1_struct_0(sK22))
& ~ v3_struct_0(sK23)
& v2_orders_2(sK23)
& v3_orders_2(sK23)
& v4_orders_2(sK23)
& v1_lattice3(sK23)
& l1_orders_2(sK23)
& ~ v3_struct_0(sK22)
& v2_orders_2(sK22)
& v3_orders_2(sK22)
& v4_orders_2(sK22)
& v1_lattice3(sK22)
& l1_orders_2(sK22) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24,sK25,sK26,sK27]),skolemize(X0,sK22),skolemize(X1,sK23),skolemize(X2,sK24),skolemize(X3,sK25),skolemize(X4,sK26),skolemize(X5,sK27)],[f19089]) ).
fof(f20181,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f20182,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(flattening,[],[f20181]) ).
fof(f20183,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(rectify,[],[f20182]) ).
fof(f20184,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK33(X0,X1,X2),X0)
| ~ r2_hidden(sK33(X0,X1,X2),X1)
| ~ r2_hidden(sK33(X0,X1,X2),X2) )
& ( ( r2_hidden(sK33(X0,X1,X2),X0)
& r2_hidden(sK33(X0,X1,X2),X1) )
| r2_hidden(sK33(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(X3,sK33(X0,X1,X2))],[f20183]) ).
fof(f20197,plain,
! [X0] :
( ! [X1] :
( ( ( v12_waybel_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(X3,X1)
& r2_hidden(X2,X1)
& r1_orders_2(X0,X3,X2)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| ~ r1_orders_2(X0,X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v12_waybel_0(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f19150]) ).
fof(f20198,plain,
! [X0] :
( ! [X1] :
( ( ( v12_waybel_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(X3,X1)
& r2_hidden(X2,X1)
& r1_orders_2(X0,X3,X2)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X5,X4)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ v12_waybel_0(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f20197]) ).
fof(f20199,plain,
! [X0] :
( ! [X1] :
( ( ( v12_waybel_0(X1,X0)
| ( ~ r2_hidden(sK43(X0,X1),X1)
& r2_hidden(sK42(X0,X1),X1)
& r1_orders_2(X0,sK43(X0,X1),sK42(X0,X1))
& m1_subset_1(sK43(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK42(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X5,X4)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ v12_waybel_0(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42,sK43]),skolemize(X2,sK42(X0,X1)),skolemize(X3,sK43(X0,X1))],[f20198]) ).
fof(f20204,plain,
! [X0] :
( ! [X1] :
( ( ( v13_waybel_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(X3,X1)
& r2_hidden(X2,X1)
& r1_orders_2(X0,X2,X3)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| ~ r1_orders_2(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v13_waybel_0(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f19163]) ).
fof(f20205,plain,
! [X0] :
( ! [X1] :
( ( ( v13_waybel_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(X3,X1)
& r2_hidden(X2,X1)
& r1_orders_2(X0,X2,X3)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ v13_waybel_0(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f20204]) ).
fof(f20206,plain,
! [X0] :
( ! [X1] :
( ( ( v13_waybel_0(X1,X0)
| ( ~ r2_hidden(sK49(X0,X1),X1)
& r2_hidden(sK48(X0,X1),X1)
& r1_orders_2(X0,sK48(X0,X1),sK49(X0,X1))
& m1_subset_1(sK49(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK48(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ v13_waybel_0(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48,sK49]),skolemize(X2,sK48(X0,X1)),skolemize(X3,sK49(X0,X1))],[f20205]) ).
fof(f20207,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( ( r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X1,X4,X5) )
& ( r1_orders_2(X1,X4,X5)
| ~ r1_orders_2(X0,X2,X3) ) )
| X2 != X4
| X3 != X5
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f19165]) ).
fof(f20218,plain,
! [X0] :
( ! [X1] :
( ( ( v1_waybel_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k13_lattice3(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( r2_hidden(k13_lattice3(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v1_waybel_0(X1,X0) ) )
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f19210]) ).
fof(f20219,plain,
! [X0] :
( ! [X1] :
( ( ( v1_waybel_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k13_lattice3(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( r2_hidden(k13_lattice3(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ v1_waybel_0(X1,X0) ) )
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f20218]) ).
fof(f20220,plain,
! [X0] :
( ! [X1] :
( ( ( v1_waybel_0(X1,X0)
| ( ~ r2_hidden(k13_lattice3(X0,sK53(X0,X1),sK54(X0,X1)),X1)
& r2_hidden(sK53(X0,X1),X1)
& r2_hidden(sK54(X0,X1),X1)
& m1_subset_1(sK54(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK53(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( r2_hidden(k13_lattice3(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ v1_waybel_0(X1,X0) ) )
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53,sK54]),skolemize(X2,sK53(X0,X1)),skolemize(X3,sK54(X0,X1))],[f20219]) ).
fof(f20221,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X1 = k13_lattice3(X0,X1,X2)
| ~ r1_orders_2(X0,X2,X1) )
& ( r1_orders_2(X0,X2,X1)
| k13_lattice3(X0,X1,X2) != X1 ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f19212]) ).
fof(f20222,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k13_lattice3(X0,X1,X2)
| ~ r1_orders_2(X0,X1,X3)
| ~ r1_orders_2(X0,X2,X3)
| ? [X4] :
( ~ r1_orders_2(X0,X3,X4)
& r1_orders_2(X0,X1,X4)
& r1_orders_2(X0,X2,X4)
& m1_subset_1(X4,u1_struct_0(X0)) ) )
& ( ( r1_orders_2(X0,X1,X3)
& r1_orders_2(X0,X2,X3)
& ! [X4] :
( r1_orders_2(X0,X3,X4)
| ~ r1_orders_2(X0,X1,X4)
| ~ r1_orders_2(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| k13_lattice3(X0,X1,X2) != X3 ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f19214]) ).
fof(f20223,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k13_lattice3(X0,X1,X2)
| ~ r1_orders_2(X0,X1,X3)
| ~ r1_orders_2(X0,X2,X3)
| ? [X4] :
( ~ r1_orders_2(X0,X3,X4)
& r1_orders_2(X0,X1,X4)
& r1_orders_2(X0,X2,X4)
& m1_subset_1(X4,u1_struct_0(X0)) ) )
& ( ( r1_orders_2(X0,X1,X3)
& r1_orders_2(X0,X2,X3)
& ! [X4] :
( r1_orders_2(X0,X3,X4)
| ~ r1_orders_2(X0,X1,X4)
| ~ r1_orders_2(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| k13_lattice3(X0,X1,X2) != X3 ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f20222]) ).
fof(f20224,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k13_lattice3(X0,X1,X2)
| ~ r1_orders_2(X0,X1,X3)
| ~ r1_orders_2(X0,X2,X3)
| ? [X4] :
( ~ r1_orders_2(X0,X3,X4)
& r1_orders_2(X0,X1,X4)
& r1_orders_2(X0,X2,X4)
& m1_subset_1(X4,u1_struct_0(X0)) ) )
& ( ( r1_orders_2(X0,X1,X3)
& r1_orders_2(X0,X2,X3)
& ! [X5] :
( r1_orders_2(X0,X3,X5)
| ~ r1_orders_2(X0,X1,X5)
| ~ r1_orders_2(X0,X2,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0)) ) )
| k13_lattice3(X0,X1,X2) != X3 ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f20223]) ).
fof(f20225,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k13_lattice3(X0,X1,X2)
| ~ r1_orders_2(X0,X1,X3)
| ~ r1_orders_2(X0,X2,X3)
| ( ~ r1_orders_2(X0,X3,sK55(X0,X1,X2,X3))
& r1_orders_2(X0,X1,sK55(X0,X1,X2,X3))
& r1_orders_2(X0,X2,sK55(X0,X1,X2,X3))
& m1_subset_1(sK55(X0,X1,X2,X3),u1_struct_0(X0)) ) )
& ( ( r1_orders_2(X0,X1,X3)
& r1_orders_2(X0,X2,X3)
& ! [X5] :
( r1_orders_2(X0,X3,X5)
| ~ r1_orders_2(X0,X1,X5)
| ~ r1_orders_2(X0,X2,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0)) ) )
| k13_lattice3(X0,X1,X2) != X3 ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55]),skolemize(X4,sK55(X0,X1,X2,X3))],[f20224]) ).
fof(f20364,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f19538]) ).
fof(f20627,plain,
l1_orders_2(sK22),
inference(cnf_transformation,[],[f20177]) ).
fof(f20628,plain,
v1_lattice3(sK22),
inference(cnf_transformation,[],[f20177]) ).
fof(f20629,plain,
v4_orders_2(sK22),
inference(cnf_transformation,[],[f20177]) ).
fof(f20630,plain,
v3_orders_2(sK22),
inference(cnf_transformation,[],[f20177]) ).
fof(f20631,plain,
v2_orders_2(sK22),
inference(cnf_transformation,[],[f20177]) ).
fof(f20632,plain,
~ v3_struct_0(sK22),
inference(cnf_transformation,[],[f20177]) ).
fof(f20633,plain,
l1_orders_2(sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20634,plain,
v1_lattice3(sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20635,plain,
v4_orders_2(sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20636,plain,
v3_orders_2(sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20637,plain,
v2_orders_2(sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20638,plain,
~ v3_struct_0(sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20639,plain,
m1_subset_1(sK24,u1_struct_0(sK22)),
inference(cnf_transformation,[],[f20177]) ).
fof(f20640,plain,
m1_subset_1(sK25,u1_struct_0(sK22)),
inference(cnf_transformation,[],[f20177]) ).
fof(f20641,plain,
m1_subset_1(sK26,u1_struct_0(sK23)),
inference(cnf_transformation,[],[f20177]) ).
fof(f20642,plain,
m1_subset_1(sK27,u1_struct_0(sK23)),
inference(cnf_transformation,[],[f20177]) ).
fof(f20643,plain,
sK25 = sK27,
inference(cnf_transformation,[],[f20177]) ).
fof(f20644,plain,
sK24 = sK26,
inference(cnf_transformation,[],[f20177]) ).
fof(f20645,plain,
r1_latsum_1(sK22,sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20646,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),k1_zfmisc_1(u1_struct_0(sK22))),
inference(cnf_transformation,[],[f20177]) ).
fof(f20647,plain,
v13_waybel_0(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),sK22),
inference(cnf_transformation,[],[f20177]) ).
fof(f20648,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),k1_zfmisc_1(u1_struct_0(sK23))),
inference(cnf_transformation,[],[f20177]) ).
fof(f20649,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20650,plain,
v1_waybel_0(k3_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)),sK23),
inference(cnf_transformation,[],[f20177]) ).
fof(f20651,plain,
k13_lattice3(sK22,sK24,sK25) != k13_lattice3(sK23,sK26,sK27),
inference(cnf_transformation,[],[f20177]) ).
fof(f20707,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f20184]) ).
fof(f20713,plain,
! [X0] :
( ~ v1_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19128]) ).
fof(f20721,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19132]) ).
fof(f20745,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X5,X4)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20199]) ).
fof(f20772,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v13_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20206]) ).
fof(f20778,plain,
! [X2,X3,X0,X1,X4,X5] :
( r1_orders_2(X1,X4,X5)
| ~ r1_orders_2(X0,X2,X3)
| X2 != X4
| X3 != X5
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20207]) ).
fof(f20779,plain,
! [X2,X3,X0,X1,X4,X5] :
( r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X1,X4,X5)
| X2 != X4
| X3 != X5
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20207]) ).
fof(f20809,plain,
! [X2,X3,X0,X1] :
( ~ r1_orders_2(X0,k13_lattice3(X0,X1,X2),X3)
| r1_orders_2(X0,X1,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19199]) ).
fof(f20810,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k13_lattice3(X0,X1,X1) = X1
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19201]) ).
fof(f20813,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,k13_lattice3(X0,X1,X3),k13_lattice3(X0,X2,X3))
| ~ r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19207]) ).
fof(f20816,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k13_lattice3(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v1_waybel_0(X1,X0)
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20220]) ).
fof(f20823,plain,
! [X2,X0,X1] :
( ~ r1_orders_2(X0,X2,X1)
| k13_lattice3(X0,X1,X2) = X1
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20221]) ).
fof(f20824,plain,
! [X2,X3,X0,X1,X5] :
( r1_orders_2(X0,X3,X5)
| ~ r1_orders_2(X0,X1,X5)
| ~ r1_orders_2(X0,X2,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| k13_lattice3(X0,X1,X2) != X3
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20225]) ).
fof(f20825,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,X2,X3)
| k13_lattice3(X0,X1,X2) != X3
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20225]) ).
fof(f20826,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,X1,X3)
| k13_lattice3(X0,X1,X2) != X3
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20225]) ).
fof(f20831,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k13_lattice3(X0,X1,X2) = k13_lattice3(X0,X2,X1) ),
inference(cnf_transformation,[],[f19216]) ).
fof(f20832,plain,
! [X2,X0,X1] :
( m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19218]) ).
fof(f20839,plain,
! [X2,X0,X1] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(cnf_transformation,[],[f19228]) ).
fof(f21334,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f20364]) ).
fof(f21364,plain,
! [X0] : k1_zfmisc_1(X0) = u1_struct_0(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f16349]) ).
fof(f21547,plain,
! [X2,X0,X1] :
( ~ r1_orders_2(X0,X2,X1)
| ~ r1_orders_2(X0,X1,X2)
| X1 = X2
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19675]) ).
fof(f22047,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f22315,plain,
k13_lattice3(sK23,sK26,sK27) != k13_lattice3(sK22,sK26,sK27),
inference(definition_unfolding,[],[f20651,f20644,f20643]) ).
fof(f22316,plain,
v1_waybel_0(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),sK23),
inference(definition_unfolding,[],[f20650,f22047]) ).
fof(f22317,plain,
v12_waybel_0(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),sK23),
inference(definition_unfolding,[],[f20649,f22047]) ).
fof(f22318,plain,
m1_subset_1(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),u1_struct_0(k3_yellow_1(u1_struct_0(sK23)))),
inference(definition_unfolding,[],[f20648,f22047,f21364]) ).
fof(f22319,plain,
v13_waybel_0(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),sK22),
inference(definition_unfolding,[],[f20647,f22047]) ).
fof(f22320,plain,
m1_subset_1(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),u1_struct_0(k3_yellow_1(u1_struct_0(sK22)))),
inference(definition_unfolding,[],[f20646,f22047,f21364]) ).
fof(f22321,plain,
m1_subset_1(sK27,u1_struct_0(sK22)),
inference(definition_unfolding,[],[f20640,f20643]) ).
fof(f22322,plain,
m1_subset_1(sK26,u1_struct_0(sK22)),
inference(definition_unfolding,[],[f20639,f20644]) ).
fof(f22376,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1)
| k4_xboole_0(X0,k4_xboole_0(X0,X1)) != X2 ),
inference(definition_unfolding,[],[f20707,f22047]) ).
fof(f22409,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X5,X4)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k3_yellow_1(u1_struct_0(X0))))
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f20745,f21364]) ).
fof(f22420,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v13_waybel_0(X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k3_yellow_1(u1_struct_0(X0))))
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f20772,f21364]) ).
fof(f22436,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k13_lattice3(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v1_waybel_0(X1,X0)
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k3_yellow_1(u1_struct_0(X0))))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f20816,f21364]) ).
fof(f22437,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k3_yellow_1(X2)))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(definition_unfolding,[],[f20839,f21364]) ).
fof(f22775,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k4_xboole_0(X0,k4_xboole_0(X0,X1)))
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f22376]) ).
fof(f22778,plain,
! [X3,X0,X1,X4,X5] :
( r1_orders_2(X0,X4,X3)
| ~ r1_orders_2(X1,X4,X5)
| X3 != X5
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f20779]) ).
fof(f22779,plain,
! [X0,X1,X4,X5] :
( ~ r1_orders_2(X1,X4,X5)
| r1_orders_2(X0,X4,X5)
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f22778]) ).
fof(f22780,plain,
! [X3,X0,X1,X4,X5] :
( r1_orders_2(X1,X4,X5)
| ~ r1_orders_2(X0,X4,X3)
| X3 != X5
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f20778]) ).
fof(f22781,plain,
! [X0,X1,X4,X5] :
( ~ r1_orders_2(X0,X4,X5)
| r1_orders_2(X1,X4,X5)
| ~ r1_latsum_1(X0,X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f22780]) ).
fof(f22790,plain,
! [X2,X0,X1] :
( r1_orders_2(X0,X1,k13_lattice3(X0,X1,X2))
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f20826]) ).
fof(f22791,plain,
! [X2,X0,X1] :
( r1_orders_2(X0,X2,k13_lattice3(X0,X1,X2))
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f20825]) ).
fof(f22792,plain,
! [X2,X0,X1,X5] :
( r1_orders_2(X0,k13_lattice3(X0,X1,X2),X5)
| ~ r1_orders_2(X0,X1,X5)
| ~ r1_orders_2(X0,X2,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f20824]) ).
fof(f22943,plain,
! [X2,X0,X1,X5] :
( r1_orders_2(X0,k13_lattice3(X0,X1,X2),X5)
| ~ r1_orders_2(X0,X1,X5)
| ~ r1_orders_2(X0,X2,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f22792,f20832]) ).
fof(f22944,plain,
! [X2,X0,X1] :
( r1_orders_2(X0,X2,k13_lattice3(X0,X1,X2))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f22791,f20832]) ).
fof(f22945,plain,
! [X2,X0,X1] :
( r1_orders_2(X0,X1,k13_lattice3(X0,X1,X2))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f22790,f20832]) ).
fof(f22946,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k13_lattice3(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ v1_waybel_0(X1,X0)
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k3_yellow_1(u1_struct_0(X0))))
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f22436,f22437]) ).
fof(f22954,plain,
! [X0,X1,X4,X5] :
( ~ m1_subset_1(X1,u1_struct_0(k3_yellow_1(u1_struct_0(X0))))
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ v13_waybel_0(X1,X0)
| r2_hidden(X5,X1)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f22420,f22437]) ).
fof(f22955,plain,
! [X0,X1,X4,X5] :
( ~ m1_subset_1(X1,u1_struct_0(k3_yellow_1(u1_struct_0(X0))))
| ~ r2_hidden(X4,X1)
| ~ r1_orders_2(X0,X5,X4)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ v12_waybel_0(X1,X0)
| r2_hidden(X5,X1)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f22409,f22437]) ).
fof(f22974,plain,
! [X0,X1,X4,X5] :
( ~ m1_subset_1(X1,u1_struct_0(k3_yellow_1(u1_struct_0(X0))))
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ v1_waybel_0(X1,X0)
| ~ v12_waybel_0(X1,X0)
| r2_hidden(k13_lattice3(X0,X4,X5),X1)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f22946,f22437]) ).
fof(f22997,plain,
! [X0] :
( ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| k13_lattice3(sK23,X0,sK27) = k13_lattice3(sK23,sK27,X0) ),
inference(resolution,[],[f20831,f20642]) ).
fof(f22998,plain,
! [X0] :
( ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| k13_lattice3(sK22,X0,sK27) = k13_lattice3(sK22,sK27,X0) ),
inference(resolution,[],[f20831,f22321]) ).
fof(f23007,plain,
! [X0] :
( ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| k13_lattice3(sK22,X0,sK27) = k13_lattice3(sK22,sK27,X0) ),
inference(forward_subsumption_resolution,[],[f22998,f20629]) ).
fof(f23008,plain,
! [X0] :
( ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| k13_lattice3(sK23,X0,sK27) = k13_lattice3(sK23,sK27,X0) ),
inference(forward_subsumption_resolution,[],[f22997,f20635]) ).
fof(f23013,plain,
! [X0] :
( ~ l1_orders_2(sK22)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| k13_lattice3(sK22,X0,sK27) = k13_lattice3(sK22,sK27,X0) ),
inference(forward_subsumption_resolution,[],[f23007,f20628]) ).
fof(f23014,plain,
! [X0] :
( ~ l1_orders_2(sK23)
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| k13_lattice3(sK23,X0,sK27) = k13_lattice3(sK23,sK27,X0) ),
inference(forward_subsumption_resolution,[],[f23008,f20634]) ).
fof(f23033,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK22))
| k13_lattice3(sK22,X0,sK27) = k13_lattice3(sK22,sK27,X0) ),
inference(forward_subsumption_resolution,[],[f23013,f20627]) ).
fof(f23034,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK23))
| k13_lattice3(sK23,X0,sK27) = k13_lattice3(sK23,sK27,X0) ),
inference(forward_subsumption_resolution,[],[f23014,f20633]) ).
fof(f23036,plain,
k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK22,sK27,sK26),
inference(resolution,[],[f23033,f22322]) ).
fof(f23040,plain,
k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,sK27,sK26),
inference(resolution,[],[f23034,f20641]) ).
fof(f23071,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ v1_waybel_0(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),sK23)
| ~ v12_waybel_0(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),sK23)
| r2_hidden(k13_lattice3(sK23,X0,X1),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23) ),
inference(resolution,[],[f22974,f22318]) ).
fof(f23072,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ v12_waybel_0(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),sK23)
| r2_hidden(k13_lattice3(sK23,X0,X1),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23) ),
inference(forward_subsumption_resolution,[],[f23071,f22316]) ).
fof(f23074,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| r2_hidden(k13_lattice3(sK23,X0,X1),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23) ),
inference(forward_subsumption_resolution,[],[f23072,f22317]) ).
fof(f23076,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| r2_hidden(k13_lattice3(sK23,X0,X1),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23) ),
inference(forward_subsumption_resolution,[],[f23074,f20635]) ).
fof(f23078,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| r2_hidden(k13_lattice3(sK23,X0,X1),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ l1_orders_2(sK23) ),
inference(forward_subsumption_resolution,[],[f23076,f20634]) ).
fof(f23091,plain,
! [X0,X1] :
( r2_hidden(k13_lattice3(sK23,X0,X1),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
inference(forward_subsumption_resolution,[],[f23078,f20633]) ).
fof(f23093,plain,
! [X2,X3,X0,X1] :
( ~ r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(X0,k13_lattice3(X0,X2,X3),k13_lattice3(X0,X1,X3))
| k13_lattice3(X0,X2,X3) = k13_lattice3(X0,X1,X3)
| ~ m1_subset_1(k13_lattice3(X0,X1,X3),u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X0,X2,X3),u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f20813,f21547]) ).
fof(f23098,plain,
! [X2,X3,X0,X1] :
( ~ r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(X0,k13_lattice3(X0,X2,X3),k13_lattice3(X0,X1,X3))
| k13_lattice3(X0,X2,X3) = k13_lattice3(X0,X1,X3)
| ~ m1_subset_1(k13_lattice3(X0,X1,X3),u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X0,X2,X3),u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f23093]) ).
fof(f23103,plain,
! [X2,X3,X0,X1] :
( ~ r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(X0,k13_lattice3(X0,X2,X3),k13_lattice3(X0,X1,X3))
| k13_lattice3(X0,X2,X3) = k13_lattice3(X0,X1,X3)
| ~ m1_subset_1(k13_lattice3(X0,X1,X3),u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f23098,f20832]) ).
fof(f23108,plain,
! [X2,X3,X0,X1] :
( ~ r1_orders_2(X0,k13_lattice3(X0,X2,X3),k13_lattice3(X0,X1,X3))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(X0,X1,X2)
| k13_lattice3(X0,X2,X3) = k13_lattice3(X0,X1,X3) ),
inference(forward_subsumption_resolution,[],[f23103,f20832]) ).
fof(f23158,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X3,X2)
| k13_lattice3(X1,X2,X0) = k13_lattice3(X1,X3,X0)
| ~ r1_orders_2(X1,X2,k13_lattice3(X1,X3,X0))
| ~ r1_orders_2(X1,X0,k13_lattice3(X1,X3,X0))
| ~ m1_subset_1(k13_lattice3(X1,X3,X0),u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ l1_orders_2(X1) ),
inference(resolution,[],[f23108,f22943]) ).
fof(f23163,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X3,X2)
| k13_lattice3(X1,X2,X0) = k13_lattice3(X1,X3,X0)
| ~ r1_orders_2(X1,X2,k13_lattice3(X1,X3,X0))
| ~ r1_orders_2(X1,X0,k13_lattice3(X1,X3,X0))
| ~ m1_subset_1(k13_lattice3(X1,X3,X0),u1_struct_0(X1)) ),
inference(duplicate_literal_removal,[],[f23158]) ).
fof(f23170,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X3,X2)
| k13_lattice3(X1,X2,X0) = k13_lattice3(X1,X3,X0)
| ~ r1_orders_2(X1,X2,k13_lattice3(X1,X3,X0))
| ~ m1_subset_1(k13_lattice3(X1,X3,X0),u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f23163,f22944]) ).
fof(f23176,plain,
! [X2,X3,X0,X1] :
( ~ r1_orders_2(X1,X2,k13_lattice3(X1,X3,X0))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X3,X2)
| k13_lattice3(X1,X2,X0) = k13_lattice3(X1,X3,X0)
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f23170,f20832]) ).
fof(f23284,plain,
( sK26 = k13_lattice3(sK22,sK26,sK26)
| ~ v2_orders_2(sK22)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(resolution,[],[f20810,f22322]) ).
fof(f23286,plain,
( sK27 = k13_lattice3(sK22,sK27,sK27)
| ~ v2_orders_2(sK22)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(resolution,[],[f20810,f22321]) ).
fof(f23288,plain,
( sK27 = k13_lattice3(sK22,sK27,sK27)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f23286,f20631]) ).
fof(f23290,plain,
( sK26 = k13_lattice3(sK22,sK26,sK26)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f23284,f20631]) ).
fof(f23292,plain,
( sK27 = k13_lattice3(sK22,sK27,sK27)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f23288,f20629]) ).
fof(f23294,plain,
( sK26 = k13_lattice3(sK22,sK26,sK26)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f23290,f20629]) ).
fof(f23296,plain,
( sK27 = k13_lattice3(sK22,sK27,sK27)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f23292,f20628]) ).
fof(f23298,plain,
( sK26 = k13_lattice3(sK22,sK26,sK26)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f23294,f20628]) ).
fof(f23300,plain,
sK27 = k13_lattice3(sK22,sK27,sK27),
inference(forward_subsumption_resolution,[],[f23296,f20627]) ).
fof(f23302,plain,
sK26 = k13_lattice3(sK22,sK26,sK26),
inference(forward_subsumption_resolution,[],[f23298,f20627]) ).
fof(f23556,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,X1,k13_lattice3(X2,X3,X1))
| ~ r1_latsum_1(X0,X2)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X2)
| ~ m1_subset_1(k13_lattice3(X2,X3,X1),u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(k13_lattice3(X2,X3,X1),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2)
| ~ l1_orders_2(X2) ),
inference(resolution,[],[f22779,f22944]) ).
fof(f23557,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,X1,k13_lattice3(X2,X1,X3))
| ~ r1_latsum_1(X0,X2)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X2)
| ~ m1_subset_1(k13_lattice3(X2,X1,X3),u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(k13_lattice3(X2,X1,X3),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2)
| ~ l1_orders_2(X2) ),
inference(resolution,[],[f22779,f22945]) ).
fof(f23572,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,X1,k13_lattice3(X2,X1,X3))
| ~ r1_latsum_1(X0,X2)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X2)
| ~ m1_subset_1(k13_lattice3(X2,X1,X3),u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(k13_lattice3(X2,X1,X3),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2) ),
inference(duplicate_literal_removal,[],[f23557]) ).
fof(f23573,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,X1,k13_lattice3(X2,X3,X1))
| ~ r1_latsum_1(X0,X2)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X2)
| ~ m1_subset_1(k13_lattice3(X2,X3,X1),u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(k13_lattice3(X2,X3,X1),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2) ),
inference(duplicate_literal_removal,[],[f23556]) ).
fof(f23581,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,X1,k13_lattice3(X2,X1,X3))
| ~ r1_latsum_1(X0,X2)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X2)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(k13_lattice3(X2,X1,X3),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2) ),
inference(forward_subsumption_resolution,[],[f23572,f20832]) ).
fof(f23582,plain,
! [X2,X3,X0,X1] :
( r1_orders_2(X0,X1,k13_lattice3(X2,X3,X1))
| ~ r1_latsum_1(X0,X2)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X2)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(k13_lattice3(X2,X3,X1),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X2)
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2) ),
inference(forward_subsumption_resolution,[],[f23573,f20832]) ).
fof(f23590,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(k13_lattice3(X2,X1,X3),u1_struct_0(X0))
| ~ r1_latsum_1(X0,X2)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X2)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| r1_orders_2(X0,X1,k13_lattice3(X2,X1,X3))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2) ),
inference(forward_subsumption_resolution,[],[f23581,f20713]) ).
fof(f23591,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(k13_lattice3(X2,X3,X1),u1_struct_0(X0))
| ~ r1_latsum_1(X0,X2)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X2)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| r1_orders_2(X0,X1,k13_lattice3(X2,X3,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X2)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2) ),
inference(forward_subsumption_resolution,[],[f23582,f20713]) ).
fof(f23687,plain,
! [X2,X3,X0,X1,X4] :
( r1_orders_2(X0,k13_lattice3(X1,X2,X3),X4)
| ~ r1_latsum_1(X1,X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X1,X2,X3),u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(k13_lattice3(X1,X2,X3),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X2,X4)
| ~ r1_orders_2(X1,X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ l1_orders_2(X1) ),
inference(resolution,[],[f22781,f22943]) ).
fof(f23696,plain,
! [X2,X3,X0,X1,X4] :
( r1_orders_2(X0,k13_lattice3(X1,X2,X3),X4)
| ~ r1_latsum_1(X1,X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X1,X2,X3),u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(k13_lattice3(X1,X2,X3),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X2,X4)
| ~ r1_orders_2(X1,X3,X4)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1) ),
inference(duplicate_literal_removal,[],[f23687]) ).
fof(f23705,plain,
! [X2,X3,X0,X1,X4] :
( r1_orders_2(X0,k13_lattice3(X1,X2,X3),X4)
| ~ r1_latsum_1(X1,X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X1,X2,X3),u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X2,X4)
| ~ r1_orders_2(X1,X3,X4)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1) ),
inference(forward_subsumption_resolution,[],[f23696,f20832]) ).
fof(f23714,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(k13_lattice3(X1,X2,X3),u1_struct_0(X0))
| ~ r1_latsum_1(X1,X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| r1_orders_2(X0,k13_lattice3(X1,X2,X3),X4)
| ~ m1_subset_1(X4,u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ r1_orders_2(X1,X2,X4)
| ~ r1_orders_2(X1,X3,X4)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1) ),
inference(forward_subsumption_resolution,[],[f23705,f20713]) ).
fof(f23732,plain,
! [X0,X1] :
( ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK27,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK27,X1)
| ~ r1_orders_2(sK22,sK27,X1)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(superposition,[],[f23714,f23300]) ).
fof(f23734,plain,
! [X0,X1] :
( ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK26,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X1)
| ~ r1_orders_2(sK22,sK26,X1)
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(superposition,[],[f23714,f23302]) ).
fof(f23737,plain,
! [X0,X1] :
( ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK26,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X1)
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(duplicate_literal_removal,[],[f23734]) ).
fof(f23739,plain,
! [X0,X1] :
( ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK27,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK27,X1)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(duplicate_literal_removal,[],[f23732]) ).
fof(f23742,plain,
! [X0,X1] :
( ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK26,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X1)
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(forward_subsumption_resolution,[],[f23737,f20630]) ).
fof(f23744,plain,
! [X0,X1] :
( ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK27,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK27,X1)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(forward_subsumption_resolution,[],[f23739,f20630]) ).
fof(f23746,plain,
! [X0,X1] :
( ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK26,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(sK22,sK26,X1)
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(forward_subsumption_resolution,[],[f23742,f20627]) ).
fof(f23748,plain,
! [X0,X1] :
( ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK27,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(sK22,sK27,X1)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(forward_subsumption_resolution,[],[f23744,f20627]) ).
fof(f23750,plain,
! [X0,X1] :
( ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK26,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(sK22,sK26,X1)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(forward_subsumption_resolution,[],[f23746,f22322]) ).
fof(f23752,plain,
! [X0,X1] :
( ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK27,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(sK22,sK27,X1)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) ),
inference(forward_subsumption_resolution,[],[f23748,f22321]) ).
fof(f23754,plain,
! [X0,X1] :
( ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK26,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(sK22,sK26,X1)
| ~ v1_lattice3(sK22) ),
inference(forward_subsumption_resolution,[],[f23750,f20629]) ).
fof(f23756,plain,
! [X0,X1] :
( ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK27,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ r1_orders_2(sK22,sK27,X1)
| ~ v1_lattice3(sK22) ),
inference(forward_subsumption_resolution,[],[f23752,f20629]) ).
fof(f23758,plain,
! [X0,X1] :
( ~ r1_orders_2(sK22,sK26,X1)
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK26,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK26,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f23754,f20628]) ).
fof(f23760,plain,
! [X0,X1] :
( ~ r1_orders_2(sK22,sK27,X1)
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_orders_2(X0,sK27,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK27,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f23756,f20628]) ).
fof(f23791,plain,
! [X0] :
( ~ r1_orders_2(sK23,X0,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v3_orders_2(sK23)
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ r1_orders_2(sK23,sK27,X0)
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,X0,sK26)
| ~ m1_subset_1(sK26,u1_struct_0(sK23)) ),
inference(superposition,[],[f23176,f23040]) ).
fof(f23805,plain,
! [X0] :
( ~ r1_orders_2(sK23,X0,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| ~ v3_orders_2(sK23)
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ r1_orders_2(sK23,sK27,X0)
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,X0,sK26)
| ~ m1_subset_1(sK26,u1_struct_0(sK23)) ),
inference(forward_subsumption_resolution,[],[f23791,f20642]) ).
fof(f23810,plain,
! [X0] :
( ~ r1_orders_2(sK23,X0,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ r1_orders_2(sK23,sK27,X0)
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,X0,sK26)
| ~ m1_subset_1(sK26,u1_struct_0(sK23)) ),
inference(forward_subsumption_resolution,[],[f23805,f20636]) ).
fof(f23813,plain,
! [X0] :
( ~ r1_orders_2(sK23,X0,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ r1_orders_2(sK23,sK27,X0)
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,X0,sK26)
| ~ m1_subset_1(sK26,u1_struct_0(sK23)) ),
inference(forward_subsumption_resolution,[],[f23810,f20635]) ).
fof(f23815,plain,
! [X0] :
( ~ r1_orders_2(sK23,X0,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| ~ l1_orders_2(sK23)
| ~ r1_orders_2(sK23,sK27,X0)
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,X0,sK26)
| ~ m1_subset_1(sK26,u1_struct_0(sK23)) ),
inference(forward_subsumption_resolution,[],[f23813,f20634]) ).
fof(f23817,plain,
! [X0] :
( ~ r1_orders_2(sK23,X0,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| ~ r1_orders_2(sK23,sK27,X0)
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,X0,sK26)
| ~ m1_subset_1(sK26,u1_struct_0(sK23)) ),
inference(forward_subsumption_resolution,[],[f23815,f20633]) ).
fof(f23819,plain,
! [X0] :
( ~ r1_orders_2(sK23,X0,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| ~ r1_orders_2(sK23,sK27,X0)
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,X0,sK26) ),
inference(forward_subsumption_resolution,[],[f23817,f20641]) ).
fof(f23848,plain,
! [X0] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| m1_subset_1(X0,u1_struct_0(sK22)) ),
inference(resolution,[],[f22437,f22320]) ).
fof(f23849,plain,
! [X0] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| m1_subset_1(X0,u1_struct_0(sK23)) ),
inference(resolution,[],[f22437,f22318]) ).
fof(f24046,plain,
! [X0] :
( ~ r1_orders_2(sK22,k13_lattice3(sK22,sK26,sK27),X0)
| r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ v3_orders_2(sK22)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(superposition,[],[f20809,f23036]) ).
fof(f24062,plain,
! [X0] :
( ~ r1_orders_2(sK22,k13_lattice3(sK22,sK26,sK27),X0)
| r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ v3_orders_2(sK22)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f24046,f22322]) ).
fof(f24068,plain,
! [X0] :
( ~ r1_orders_2(sK22,k13_lattice3(sK22,sK26,sK27),X0)
| r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ v3_orders_2(sK22)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f24062,f22321]) ).
fof(f24070,plain,
! [X0] :
( ~ r1_orders_2(sK22,k13_lattice3(sK22,sK26,sK27),X0)
| r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f24068,f20630]) ).
fof(f24072,plain,
! [X0] :
( ~ r1_orders_2(sK22,k13_lattice3(sK22,sK26,sK27),X0)
| r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f24070,f20629]) ).
fof(f24074,plain,
! [X0] :
( ~ r1_orders_2(sK22,k13_lattice3(sK22,sK26,sK27),X0)
| r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f24072,f20628]) ).
fof(f24076,plain,
! [X0] :
( ~ r1_orders_2(sK22,k13_lattice3(sK22,sK26,sK27),X0)
| r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22)) ),
inference(forward_subsumption_resolution,[],[f24074,f20627]) ).
fof(f24250,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r1_orders_2(sK22,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ v13_waybel_0(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),sK22)
| r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ l1_orders_2(sK22) ),
inference(resolution,[],[f22954,f22320]) ).
fof(f24255,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r1_orders_2(sK22,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f24250,f22319]) ).
fof(f24265,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r1_orders_2(sK22,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
inference(forward_subsumption_resolution,[],[f24255,f20627]) ).
fof(f24268,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r1_orders_2(sK23,X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(sK23))
| ~ v12_waybel_0(k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))),sK23)
| r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ l1_orders_2(sK23) ),
inference(resolution,[],[f22955,f22318]) ).
fof(f24271,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r1_orders_2(sK23,X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(sK23))
| r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ l1_orders_2(sK23) ),
inference(forward_subsumption_resolution,[],[f24268,f22317]) ).
fof(f24273,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r1_orders_2(sK23,X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(sK23))
| r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
inference(forward_subsumption_resolution,[],[f24271,f20633]) ).
fof(f24674,plain,
( r2_hidden(sK26,u1_struct_0(sK23))
| v1_xboole_0(u1_struct_0(sK23)) ),
inference(resolution,[],[f21334,f20641]) ).
fof(f24675,plain,
( r2_hidden(sK26,u1_struct_0(sK22))
| v1_xboole_0(u1_struct_0(sK22)) ),
inference(resolution,[],[f21334,f22322]) ).
fof(f24676,plain,
( r2_hidden(sK27,u1_struct_0(sK23))
| v1_xboole_0(u1_struct_0(sK23)) ),
inference(resolution,[],[f21334,f20642]) ).
fof(f24677,plain,
( r2_hidden(sK27,u1_struct_0(sK22))
| v1_xboole_0(u1_struct_0(sK22)) ),
inference(resolution,[],[f21334,f22321]) ).
fof(f24679,definition,
( spl329_14
<=> v1_xboole_0(u1_struct_0(sK22)) ),
introduced(definition,[new_symbols(definition,[spl329_14])],[avatar_definition]) ).
fof(f24680,plain,
( ~ v1_xboole_0(u1_struct_0(sK22))
| spl329_14 ),
inference(avatar_component_clause,[],[f24679]) ).
fof(f24681,plain,
( v1_xboole_0(u1_struct_0(sK22))
| ~ spl329_14 ),
inference(avatar_component_clause,[],[f24679]) ).
fof(f24683,definition,
( spl329_15
<=> r2_hidden(sK27,u1_struct_0(sK22)) ),
introduced(definition,[new_symbols(definition,[spl329_15])],[avatar_definition]) ).
fof(f24685,plain,
( r2_hidden(sK27,u1_struct_0(sK22))
| ~ spl329_15 ),
inference(avatar_component_clause,[],[f24683]) ).
fof(f24686,plain,
( spl329_14
| spl329_15 ),
inference(avatar_split_clause,[],[f24677,f24683,f24679]) ).
fof(f24688,definition,
( spl329_16
<=> v1_xboole_0(u1_struct_0(sK23)) ),
introduced(definition,[new_symbols(definition,[spl329_16])],[avatar_definition]) ).
fof(f24689,plain,
( ~ v1_xboole_0(u1_struct_0(sK23))
| spl329_16 ),
inference(avatar_component_clause,[],[f24688]) ).
fof(f24690,plain,
( v1_xboole_0(u1_struct_0(sK23))
| ~ spl329_16 ),
inference(avatar_component_clause,[],[f24688]) ).
fof(f24692,definition,
( spl329_17
<=> r2_hidden(sK27,u1_struct_0(sK23)) ),
introduced(definition,[new_symbols(definition,[spl329_17])],[avatar_definition]) ).
fof(f24694,plain,
( r2_hidden(sK27,u1_struct_0(sK23))
| ~ spl329_17 ),
inference(avatar_component_clause,[],[f24692]) ).
fof(f24695,plain,
( spl329_16
| spl329_17 ),
inference(avatar_split_clause,[],[f24676,f24692,f24688]) ).
fof(f24697,definition,
( spl329_18
<=> r2_hidden(sK26,u1_struct_0(sK22)) ),
introduced(definition,[new_symbols(definition,[spl329_18])],[avatar_definition]) ).
fof(f24699,plain,
( r2_hidden(sK26,u1_struct_0(sK22))
| ~ spl329_18 ),
inference(avatar_component_clause,[],[f24697]) ).
fof(f24700,plain,
( spl329_14
| spl329_18 ),
inference(avatar_split_clause,[],[f24675,f24697,f24679]) ).
fof(f24702,definition,
( spl329_19
<=> r2_hidden(sK26,u1_struct_0(sK23)) ),
introduced(definition,[new_symbols(definition,[spl329_19])],[avatar_definition]) ).
fof(f24704,plain,
( r2_hidden(sK26,u1_struct_0(sK23))
| ~ spl329_19 ),
inference(avatar_component_clause,[],[f24702]) ).
fof(f24705,plain,
( spl329_16
| spl329_19 ),
inference(avatar_split_clause,[],[f24674,f24702,f24688]) ).
fof(f24709,plain,
( v3_struct_0(sK23)
| ~ v2_orders_2(sK23)
| ~ v3_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_16 ),
inference(resolution,[],[f24690,f20721]) ).
fof(f24712,plain,
( ~ v2_orders_2(sK23)
| ~ v3_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_16 ),
inference(forward_subsumption_resolution,[],[f24709,f20638]) ).
fof(f24715,plain,
( ~ v3_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_16 ),
inference(forward_subsumption_resolution,[],[f24712,f20637]) ).
fof(f24716,plain,
( ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_16 ),
inference(forward_subsumption_resolution,[],[f24715,f20636]) ).
fof(f24717,plain,
( ~ l1_orders_2(sK23)
| ~ spl329_16 ),
inference(forward_subsumption_resolution,[],[f24716,f20634]) ).
fof(f24718,plain,
( $false
| ~ spl329_16 ),
inference(forward_subsumption_resolution,[],[f24717,f20633]) ).
fof(f24719,plain,
~ spl329_16,
inference(avatar_contradiction_clause,[],[f24718]) ).
fof(f24720,plain,
( v3_struct_0(sK22)
| ~ v2_orders_2(sK22)
| ~ v3_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ spl329_14 ),
inference(resolution,[],[f24681,f20721]) ).
fof(f24723,plain,
( ~ v2_orders_2(sK22)
| ~ v3_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ spl329_14 ),
inference(forward_subsumption_resolution,[],[f24720,f20632]) ).
fof(f24726,plain,
( ~ v3_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ spl329_14 ),
inference(forward_subsumption_resolution,[],[f24723,f20631]) ).
fof(f24727,plain,
( ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ spl329_14 ),
inference(forward_subsumption_resolution,[],[f24726,f20630]) ).
fof(f24728,plain,
( ~ l1_orders_2(sK22)
| ~ spl329_14 ),
inference(forward_subsumption_resolution,[],[f24727,f20628]) ).
fof(f24729,plain,
( $false
| ~ spl329_14 ),
inference(forward_subsumption_resolution,[],[f24728,f20627]) ).
fof(f24730,plain,
~ spl329_14,
inference(avatar_contradiction_clause,[],[f24729]) ).
fof(f25556,plain,
! [X0,X1] :
( ~ r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| m1_subset_1(k13_lattice3(sK23,X0,X1),u1_struct_0(sK22))
| ~ r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
inference(resolution,[],[f23848,f23091]) ).
fof(f26352,plain,
! [X0,X1] :
( ~ r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ r2_hidden(X0,u1_struct_0(sK23))
| m1_subset_1(k13_lattice3(sK23,X1,X0),u1_struct_0(sK22))
| ~ r2_hidden(X0,u1_struct_0(sK22)) ),
inference(resolution,[],[f22775,f25556]) ).
fof(f26356,plain,
! [X0,X1] :
( ~ r1_orders_2(sK23,X1,X0)
| ~ r2_hidden(X0,u1_struct_0(sK23))
| ~ r2_hidden(X0,u1_struct_0(sK22))
| ~ m1_subset_1(X1,u1_struct_0(sK23))
| r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
inference(resolution,[],[f22775,f24273]) ).
fof(f26357,plain,
! [X0,X1] :
( ~ r1_orders_2(sK22,X0,X1)
| ~ r2_hidden(X0,u1_struct_0(sK23))
| ~ r2_hidden(X0,u1_struct_0(sK22))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| r2_hidden(X1,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
inference(resolution,[],[f22775,f24265]) ).
fof(f26699,definition,
( spl329_31
<=> r2_hidden(sK26,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
introduced(definition,[new_symbols(definition,[spl329_31])],[avatar_definition]) ).
fof(f26701,plain,
( r2_hidden(sK26,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_31 ),
inference(avatar_component_clause,[],[f26699]) ).
fof(f26719,definition,
( spl329_35
<=> r2_hidden(k13_lattice3(sK23,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
introduced(definition,[new_symbols(definition,[spl329_35])],[avatar_definition]) ).
fof(f26720,plain,
( ~ r2_hidden(k13_lattice3(sK23,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| spl329_35 ),
inference(avatar_component_clause,[],[f26719]) ).
fof(f26721,plain,
( r2_hidden(k13_lattice3(sK23,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_35 ),
inference(avatar_component_clause,[],[f26719]) ).
fof(f26726,definition,
( spl329_37
<=> m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22)) ),
introduced(definition,[new_symbols(definition,[spl329_37])],[avatar_definition]) ).
fof(f26727,plain,
( m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| ~ spl329_37 ),
inference(avatar_component_clause,[],[f26726]) ).
fof(f26728,plain,
( ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| spl329_37 ),
inference(avatar_component_clause,[],[f26726]) ).
fof(f26731,definition,
( spl329_38
<=> r2_hidden(k13_lattice3(sK22,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23)))) ),
introduced(definition,[new_symbols(definition,[spl329_38])],[avatar_definition]) ).
fof(f26733,plain,
( r2_hidden(k13_lattice3(sK22,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_38 ),
inference(avatar_component_clause,[],[f26731]) ).
fof(f26786,definition,
( spl329_44
<=> m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23)) ),
introduced(definition,[new_symbols(definition,[spl329_44])],[avatar_definition]) ).
fof(f26787,plain,
( m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| ~ spl329_44 ),
inference(avatar_component_clause,[],[f26786]) ).
fof(f26788,plain,
( ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| spl329_44 ),
inference(avatar_component_clause,[],[f26786]) ).
fof(f26790,plain,
! [X0,X1] :
( m1_subset_1(k13_lattice3(sK23,X1,X0),u1_struct_0(sK22))
| ~ r2_hidden(X0,u1_struct_0(sK23))
| ~ r2_hidden(X0,u1_struct_0(sK22))
| ~ r2_hidden(X1,u1_struct_0(sK22))
| ~ r2_hidden(X1,u1_struct_0(sK23)) ),
inference(resolution,[],[f26352,f22775]) ).
fof(f26796,plain,
( ~ r2_hidden(sK27,u1_struct_0(sK23))
| ~ r2_hidden(sK27,u1_struct_0(sK22))
| ~ r2_hidden(sK26,u1_struct_0(sK22))
| ~ r2_hidden(sK26,u1_struct_0(sK23))
| spl329_37 ),
inference(resolution,[],[f26790,f26728]) ).
fof(f26835,plain,
( ~ r2_hidden(sK27,u1_struct_0(sK22))
| ~ r2_hidden(sK26,u1_struct_0(sK22))
| ~ r2_hidden(sK26,u1_struct_0(sK23))
| ~ spl329_17
| spl329_37 ),
inference(forward_subsumption_resolution,[],[f26796,f24694]) ).
fof(f26848,plain,
( ~ r2_hidden(sK26,u1_struct_0(sK22))
| ~ r2_hidden(sK26,u1_struct_0(sK23))
| ~ spl329_15
| ~ spl329_17
| spl329_37 ),
inference(forward_subsumption_resolution,[],[f26835,f24685]) ).
fof(f26858,plain,
( ~ r2_hidden(sK26,u1_struct_0(sK23))
| ~ spl329_15
| ~ spl329_17
| ~ spl329_18
| spl329_37 ),
inference(forward_subsumption_resolution,[],[f26848,f24699]) ).
fof(f26867,plain,
( $false
| ~ spl329_15
| ~ spl329_17
| ~ spl329_18
| ~ spl329_19
| spl329_37 ),
inference(forward_subsumption_resolution,[],[f26858,f24704]) ).
fof(f26868,plain,
( ~ spl329_15
| ~ spl329_17
| ~ spl329_18
| ~ spl329_19
| spl329_37 ),
inference(avatar_contradiction_clause,[],[f26867]) ).
fof(f26919,plain,
( ~ r1_latsum_1(sK22,sK23)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(sK23)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(resolution,[],[f26727,f23590]) ).
fof(f26920,plain,
( ~ r1_latsum_1(sK22,sK23)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(sK23)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(resolution,[],[f26727,f23591]) ).
fof(f26934,plain,
( r2_hidden(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| v1_xboole_0(u1_struct_0(sK22))
| ~ spl329_37 ),
inference(resolution,[],[f26727,f21334]) ).
fof(f26935,plain,
( r2_hidden(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| spl329_14
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26934,f24680]) ).
fof(f26942,plain,
( ~ v3_orders_2(sK22)
| ~ v3_orders_2(sK23)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26920,f20645]) ).
fof(f26943,plain,
( ~ v3_orders_2(sK22)
| ~ v3_orders_2(sK23)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26919,f20645]) ).
fof(f26951,plain,
( ~ v3_orders_2(sK23)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26942,f20630]) ).
fof(f26952,plain,
( ~ v3_orders_2(sK23)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26943,f20630]) ).
fof(f26959,plain,
( ~ m1_subset_1(sK27,u1_struct_0(sK23))
| r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26951,f20636]) ).
fof(f26960,plain,
( ~ m1_subset_1(sK26,u1_struct_0(sK23))
| r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26952,f20636]) ).
fof(f26966,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26959,f20642]) ).
fof(f26967,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26960,f20641]) ).
fof(f26972,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26966,f22321]) ).
fof(f26973,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ l1_orders_2(sK23)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26967,f22322]) ).
fof(f26981,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26972,f20633]) ).
fof(f26982,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26973,f20633]) ).
fof(f26985,definition,
( spl329_50
<=> r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27)) ),
introduced(definition,[new_symbols(definition,[spl329_50])],[avatar_definition]) ).
fof(f26987,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ spl329_50 ),
inference(avatar_component_clause,[],[f26985]) ).
fof(f26990,definition,
( spl329_51
<=> r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27)) ),
introduced(definition,[new_symbols(definition,[spl329_51])],[avatar_definition]) ).
fof(f26992,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ spl329_51 ),
inference(avatar_component_clause,[],[f26990]) ).
fof(f26994,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26981,f20632]) ).
fof(f26995,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26982,f20632]) ).
fof(f26997,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26994,f20627]) ).
fof(f26998,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26995,f20627]) ).
fof(f27000,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26997,f20641]) ).
fof(f27001,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f26998,f20642]) ).
fof(f27003,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f27000,f20635]) ).
fof(f27004,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ v1_lattice3(sK23)
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f27001,f20635]) ).
fof(f27006,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f27003,f20634]) ).
fof(f27007,plain,
( r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ spl329_37 ),
inference(forward_subsumption_resolution,[],[f27004,f20634]) ).
fof(f27009,plain,
( spl329_50
| ~ spl329_37 ),
inference(avatar_split_clause,[],[f27006,f26726,f26985]) ).
fof(f27010,plain,
( spl329_51
| ~ spl329_37 ),
inference(avatar_split_clause,[],[f27007,f26726,f26990]) ).
fof(f27012,plain,
( m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK23))
| ~ spl329_35 ),
inference(resolution,[],[f26721,f23849]) ).
fof(f27020,plain,
( ~ r2_hidden(sK26,u1_struct_0(sK23))
| ~ r2_hidden(sK26,u1_struct_0(sK22))
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| r2_hidden(k13_lattice3(sK23,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_51 ),
inference(resolution,[],[f26992,f26357]) ).
fof(f27027,plain,
( ! [X0] :
( r1_orders_2(X0,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(X0))
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22) )
| ~ spl329_51 ),
inference(resolution,[],[f26992,f22781]) ).
fof(f27037,plain,
( ! [X0] :
( r1_orders_2(X0,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(X0))
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22) )
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27027,f20630]) ).
fof(f27048,plain,
( ! [X0] :
( r1_orders_2(X0,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(X0))
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22) )
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27037,f26727]) ).
fof(f27058,plain,
( ! [X0] :
( r1_orders_2(X0,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(X0))
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK22)
| ~ l1_orders_2(sK22) )
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27048,f22322]) ).
fof(f27068,plain,
( ! [X0] :
( r1_orders_2(X0,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(X0))
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ l1_orders_2(sK22) )
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27058,f20632]) ).
fof(f27090,plain,
( ! [X0] :
( ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(X0))
| ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| r1_orders_2(X0,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) )
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27068,f20627]) ).
fof(f27219,plain,
( r2_hidden(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK23))
| v1_xboole_0(u1_struct_0(sK23))
| ~ spl329_35 ),
inference(resolution,[],[f27012,f21334]) ).
fof(f27229,plain,
( r2_hidden(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK23))
| spl329_16
| ~ spl329_35 ),
inference(forward_subsumption_resolution,[],[f27219,f24689]) ).
fof(f27240,plain,
( ~ r1_latsum_1(sK22,sK23)
| ~ v3_orders_2(sK23)
| r1_orders_2(sK23,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(resolution,[],[f27090,f27012]) ).
fof(f27246,plain,
( ~ v3_orders_2(sK23)
| r1_orders_2(sK23,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27240,f20645]) ).
fof(f27247,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27246,f20636]) ).
fof(f27248,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK23,sK26,sK27))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27247,f20641]) ).
fof(f27249,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ l1_orders_2(sK23)
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27248,f20638]) ).
fof(f27250,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27249,f20633]) ).
fof(f27251,plain,
( ~ r2_hidden(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK23))
| ~ r2_hidden(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| r2_hidden(sK26,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(resolution,[],[f27250,f26356]) ).
fof(f27281,plain,
( ~ r2_hidden(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| r2_hidden(sK26,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| spl329_16
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27251,f27229]) ).
fof(f27293,plain,
( ~ m1_subset_1(sK26,u1_struct_0(sK23))
| r2_hidden(sK26,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| spl329_14
| spl329_16
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27281,f26935]) ).
fof(f27304,plain,
( r2_hidden(sK26,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| spl329_14
| spl329_16
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27293,f20641]) ).
fof(f27327,plain,
( spl329_31
| spl329_14
| spl329_16
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(avatar_split_clause,[],[f27304,f26990,f26726,f26719,f24688,f24679,f26699]) ).
fof(f27351,plain,
( ! [X0] :
( r2_hidden(X0,k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ r1_orders_2(sK22,sK26,X0) )
| ~ spl329_31 ),
inference(resolution,[],[f26701,f24265]) ).
fof(f27710,plain,
( ~ r2_hidden(sK26,u1_struct_0(sK22))
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| r2_hidden(k13_lattice3(sK23,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_19
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27020,f24704]) ).
fof(f27713,plain,
( ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| r2_hidden(k13_lattice3(sK23,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_18
| ~ spl329_19
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27710,f24699]) ).
fof(f27716,plain,
( r2_hidden(k13_lattice3(sK23,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_18
| ~ spl329_19
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27713,f26727]) ).
fof(f27719,plain,
( $false
| ~ spl329_18
| ~ spl329_19
| spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(forward_subsumption_resolution,[],[f27716,f26720]) ).
fof(f27720,plain,
( ~ spl329_18
| ~ spl329_19
| spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(avatar_contradiction_clause,[],[f27719]) ).
fof(f35642,plain,
! [X0] :
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,X0,k13_lattice3(sK22,sK26,sK27)))
| ~ m1_subset_1(k13_lattice3(sK22,X0,k13_lattice3(sK22,sK26,sK27)),u1_struct_0(sK22))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(resolution,[],[f24076,f22944]) ).
fof(f35657,plain,
! [X0] :
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,X0,k13_lattice3(sK22,sK26,sK27)))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f35642,f20832]) ).
fof(f35665,plain,
! [X0] :
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,X0,k13_lattice3(sK22,sK26,sK27)))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f35657,f20629]) ).
fof(f35695,plain,
! [X0] :
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,X0,k13_lattice3(sK22,sK26,sK27)))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f35665,f20628]) ).
fof(f35699,plain,
! [X0] :
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,X0,k13_lattice3(sK22,sK26,sK27)))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(X0,u1_struct_0(sK22)) ),
inference(forward_subsumption_resolution,[],[f35695,f20627]) ).
fof(f35702,definition,
( spl329_115
<=> m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22)) ),
introduced(definition,[new_symbols(definition,[spl329_115])],[avatar_definition]) ).
fof(f35703,plain,
( m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| ~ spl329_115 ),
inference(avatar_component_clause,[],[f35702]) ).
fof(f35704,plain,
( ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| spl329_115 ),
inference(avatar_component_clause,[],[f35702]) ).
fof(f35711,definition,
( spl329_117
<=> ! [X0] :
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,X0,k13_lattice3(sK22,sK26,sK27)))
| ~ m1_subset_1(X0,u1_struct_0(sK22)) ) ),
introduced(definition,[new_symbols(definition,[spl329_117])],[avatar_definition]) ).
fof(f35712,plain,
( ! [X0] :
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,X0,k13_lattice3(sK22,sK26,sK27)))
| ~ m1_subset_1(X0,u1_struct_0(sK22)) )
| ~ spl329_117 ),
inference(avatar_component_clause,[],[f35711]) ).
fof(f35713,plain,
( ~ spl329_115
| spl329_117 ),
inference(avatar_split_clause,[],[f35699,f35711,f35702]) ).
fof(f35721,plain,
( ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| spl329_115 ),
inference(resolution,[],[f35704,f20832]) ).
fof(f35722,plain,
( ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| spl329_115 ),
inference(forward_subsumption_resolution,[],[f35721,f20629]) ).
fof(f35723,plain,
( ~ l1_orders_2(sK22)
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| spl329_115 ),
inference(forward_subsumption_resolution,[],[f35722,f20628]) ).
fof(f35724,plain,
( ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| spl329_115 ),
inference(forward_subsumption_resolution,[],[f35723,f20627]) ).
fof(f35725,plain,
( ~ m1_subset_1(sK27,u1_struct_0(sK22))
| spl329_115 ),
inference(forward_subsumption_resolution,[],[f35724,f22322]) ).
fof(f35726,plain,
( $false
| spl329_115 ),
inference(forward_subsumption_resolution,[],[f35725,f22321]) ).
fof(f35727,plain,
spl329_115,
inference(avatar_contradiction_clause,[],[f35726]) ).
fof(f35747,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK22,k13_lattice3(sK22,sK26,sK27),k13_lattice3(sK22,sK26,sK27))
| ~ v2_orders_2(sK22)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ spl329_115 ),
inference(resolution,[],[f35703,f20810]) ).
fof(f35761,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK22,k13_lattice3(sK22,sK26,sK27),k13_lattice3(sK22,sK26,sK27))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ spl329_115 ),
inference(forward_subsumption_resolution,[],[f35747,f20631]) ).
fof(f35766,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK22,k13_lattice3(sK22,sK26,sK27),k13_lattice3(sK22,sK26,sK27))
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22)
| ~ spl329_115 ),
inference(forward_subsumption_resolution,[],[f35761,f20629]) ).
fof(f35769,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK22,k13_lattice3(sK22,sK26,sK27),k13_lattice3(sK22,sK26,sK27))
| ~ l1_orders_2(sK22)
| ~ spl329_115 ),
inference(forward_subsumption_resolution,[],[f35766,f20628]) ).
fof(f35770,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK22,k13_lattice3(sK22,sK26,sK27),k13_lattice3(sK22,sK26,sK27))
| ~ spl329_115 ),
inference(forward_subsumption_resolution,[],[f35769,f20627]) ).
fof(f37521,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,sK26,X1),u1_struct_0(X0))
| r1_orders_2(X0,sK26,k13_lattice3(sK22,sK26,X1))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,X1),u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(resolution,[],[f23758,f22945]) ).
fof(f37523,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,sK26,X1),u1_struct_0(X0))
| r1_orders_2(X0,sK26,k13_lattice3(sK22,sK26,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f37521,f20832]) ).
fof(f37525,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,sK26,X1),u1_struct_0(X0))
| r1_orders_2(X0,sK26,k13_lattice3(sK22,sK26,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f37523,f22322]) ).
fof(f37527,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,sK26,X1),u1_struct_0(X0))
| r1_orders_2(X0,sK26,k13_lattice3(sK22,sK26,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f37525,f20629]) ).
fof(f37529,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,sK26,X1),u1_struct_0(X0))
| r1_orders_2(X0,sK26,k13_lattice3(sK22,sK26,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f37527,f20628]) ).
fof(f37531,plain,
! [X0,X1] :
( ~ m1_subset_1(k13_lattice3(sK22,sK26,X1),u1_struct_0(X0))
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(sK22,X0)
| r1_orders_2(X0,sK26,k13_lattice3(sK22,sK26,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK26,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22)) ),
inference(forward_subsumption_resolution,[],[f37529,f20627]) ).
fof(f38002,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,X1,sK27),u1_struct_0(X0))
| r1_orders_2(X0,sK27,k13_lattice3(sK22,X1,sK27))
| ~ m1_subset_1(k13_lattice3(sK22,X1,sK27),u1_struct_0(sK22))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(resolution,[],[f23760,f22944]) ).
fof(f38007,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,X1,sK27),u1_struct_0(X0))
| r1_orders_2(X0,sK27,k13_lattice3(sK22,X1,sK27))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f38002,f20832]) ).
fof(f38009,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,X1,sK27),u1_struct_0(X0))
| r1_orders_2(X0,sK27,k13_lattice3(sK22,X1,sK27))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f38007,f22321]) ).
fof(f38011,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,X1,sK27),u1_struct_0(X0))
| r1_orders_2(X0,sK27,k13_lattice3(sK22,X1,sK27))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ v1_lattice3(sK22)
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f38009,f20629]) ).
fof(f38013,plain,
! [X0,X1] :
( ~ r1_latsum_1(sK22,X0)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(k13_lattice3(sK22,X1,sK27),u1_struct_0(X0))
| r1_orders_2(X0,sK27,k13_lattice3(sK22,X1,sK27))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22))
| ~ l1_orders_2(sK22) ),
inference(forward_subsumption_resolution,[],[f38011,f20628]) ).
fof(f38015,plain,
! [X0,X1] :
( ~ m1_subset_1(k13_lattice3(sK22,X1,sK27),u1_struct_0(X0))
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(sK22,X0)
| r1_orders_2(X0,sK27,k13_lattice3(sK22,X1,sK27))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(sK27,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(sK22)) ),
inference(forward_subsumption_resolution,[],[f38013,f20627]) ).
fof(f38030,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ r1_orders_2(sK22,sK26,X0)
| m1_subset_1(X0,u1_struct_0(sK23)) )
| ~ spl329_31 ),
inference(resolution,[],[f27351,f23849]) ).
fof(f41225,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,sK26,sK27))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| ~ spl329_115
| ~ spl329_117 ),
inference(superposition,[],[f35712,f35770]) ).
fof(f41390,plain,
( r1_orders_2(sK22,sK27,k13_lattice3(sK22,sK26,sK27))
| ~ spl329_115
| ~ spl329_117 ),
inference(forward_subsumption_resolution,[],[f41225,f35703]) ).
fof(f41497,plain,
( ~ r2_hidden(sK27,u1_struct_0(sK23))
| ~ r2_hidden(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| r2_hidden(k13_lattice3(sK22,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_115
| ~ spl329_117 ),
inference(resolution,[],[f41390,f26357]) ).
fof(f41529,plain,
( ~ r2_hidden(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| r2_hidden(k13_lattice3(sK22,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_17
| ~ spl329_115
| ~ spl329_117 ),
inference(forward_subsumption_resolution,[],[f41497,f24694]) ).
fof(f41540,plain,
( ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK22))
| r2_hidden(k13_lattice3(sK22,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_15
| ~ spl329_17
| ~ spl329_115
| ~ spl329_117 ),
inference(forward_subsumption_resolution,[],[f41529,f24685]) ).
fof(f41548,plain,
( r2_hidden(k13_lattice3(sK22,sK26,sK27),k4_xboole_0(u1_struct_0(sK22),k4_xboole_0(u1_struct_0(sK22),u1_struct_0(sK23))))
| ~ spl329_15
| ~ spl329_17
| ~ spl329_115
| ~ spl329_117 ),
inference(forward_subsumption_resolution,[],[f41540,f35703]) ).
fof(f41560,plain,
( spl329_38
| ~ spl329_15
| ~ spl329_17
| ~ spl329_115
| ~ spl329_117 ),
inference(avatar_split_clause,[],[f41548,f35711,f35702,f24692,f24683,f26731]) ).
fof(f41571,plain,
( m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| ~ spl329_38 ),
inference(resolution,[],[f26733,f23849]) ).
fof(f41588,plain,
( $false
| ~ spl329_38
| spl329_44 ),
inference(forward_subsumption_resolution,[],[f41571,f26788]) ).
fof(f41589,plain,
( ~ spl329_38
| spl329_44 ),
inference(avatar_contradiction_clause,[],[f41588]) ).
fof(f41597,plain,
( ~ v3_orders_2(sK23)
| ~ r1_latsum_1(sK22,sK23)
| r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(resolution,[],[f26787,f37531]) ).
fof(f41599,plain,
( ~ v3_orders_2(sK23)
| ~ r1_latsum_1(sK22,sK23)
| r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(resolution,[],[f26787,f38015]) ).
fof(f41604,plain,
( ! [X0] :
( ~ r1_latsum_1(sK22,sK23)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(sK23)
| ~ m1_subset_1(X0,u1_struct_0(sK23))
| r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_44 ),
inference(resolution,[],[f26787,f23714]) ).
fof(f41636,plain,
( ! [X0] :
( ~ r1_latsum_1(sK22,sK23)
| ~ v3_orders_2(sK22)
| ~ v3_orders_2(sK23)
| r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41604,f38030]) ).
fof(f41637,plain,
( ~ r1_latsum_1(sK22,sK23)
| r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41599,f20636]) ).
fof(f41638,plain,
( ~ r1_latsum_1(sK22,sK23)
| r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41597,f20636]) ).
fof(f41653,plain,
( ! [X0] :
( ~ v3_orders_2(sK22)
| ~ v3_orders_2(sK23)
| r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41636,f20645]) ).
fof(f41654,plain,
( r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41637,f20645]) ).
fof(f41655,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41638,f20645]) ).
fof(f41667,plain,
( ! [X0] :
( ~ v3_orders_2(sK23)
| r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41653,f20630]) ).
fof(f41668,plain,
( r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41654,f20638]) ).
fof(f41669,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27))
| ~ l1_orders_2(sK23)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41655,f20638]) ).
fof(f41680,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| v3_struct_0(sK23)
| ~ l1_orders_2(sK23)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41667,f20636]) ).
fof(f41681,plain,
( r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| ~ m1_subset_1(sK27,u1_struct_0(sK23))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41668,f20633]) ).
fof(f41682,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41669,f20633]) ).
fof(f41692,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ l1_orders_2(sK23)
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41680,f20638]) ).
fof(f41693,plain,
( r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41681,f20642]) ).
fof(f41694,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27))
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41682,f20641]) ).
fof(f41704,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ l1_orders_2(sK22)
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41692,f20633]) ).
fof(f41705,plain,
( r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41693,f22322]) ).
fof(f41706,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27))
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41694,f22321]) ).
fof(f41712,definition,
( spl329_128
<=> r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27)) ),
introduced(definition,[new_symbols(definition,[spl329_128])],[avatar_definition]) ).
fof(f41714,plain,
( r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| ~ spl329_128 ),
inference(avatar_component_clause,[],[f41712]) ).
fof(f41717,definition,
( spl329_129
<=> r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27)) ),
introduced(definition,[new_symbols(definition,[spl329_129])],[avatar_definition]) ).
fof(f41719,plain,
( r1_orders_2(sK23,sK26,k13_lattice3(sK22,sK26,sK27))
| ~ spl329_129 ),
inference(avatar_component_clause,[],[f41717]) ).
fof(f41722,definition,
( spl329_130
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ r1_orders_2(sK22,sK27,X0)
| ~ r1_orders_2(sK22,sK26,X0)
| r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0) ) ),
introduced(definition,[new_symbols(definition,[spl329_130])],[avatar_definition]) ).
fof(f41723,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ r1_orders_2(sK22,sK26,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22)) )
| ~ spl329_130 ),
inference(avatar_component_clause,[],[f41722]) ).
fof(f41731,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK27,u1_struct_0(sK22))
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41704,f20627]) ).
fof(f41732,plain,
( spl329_128
| ~ spl329_44 ),
inference(avatar_split_clause,[],[f41705,f26786,f41712]) ).
fof(f41733,plain,
( spl329_129
| ~ spl329_44 ),
inference(avatar_split_clause,[],[f41706,f26786,f41717]) ).
fof(f41740,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ m1_subset_1(sK26,u1_struct_0(sK22))
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41731,f22321]) ).
fof(f41747,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ v4_orders_2(sK22)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41740,f22322]) ).
fof(f41750,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0)
| ~ v1_lattice3(sK22) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41747,f20629]) ).
fof(f41753,plain,
( ! [X0] :
( r1_orders_2(sK23,k13_lattice3(sK22,sK26,sK27),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK22))
| ~ r1_orders_2(sK22,sK26,X0)
| ~ r1_orders_2(sK22,sK27,X0) )
| ~ spl329_31
| ~ spl329_44 ),
inference(forward_subsumption_resolution,[],[f41750,f20628]) ).
fof(f41754,plain,
( spl329_130
| ~ spl329_31
| ~ spl329_44 ),
inference(avatar_split_clause,[],[f41753,f26786,f26699,f41722]) ).
fof(f41761,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ m1_subset_1(sK26,u1_struct_0(sK23))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| ~ v2_orders_2(sK23)
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_129 ),
inference(resolution,[],[f41719,f20823]) ).
fof(f41783,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| ~ v2_orders_2(sK23)
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_129 ),
inference(forward_subsumption_resolution,[],[f41761,f20641]) ).
fof(f41797,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ v2_orders_2(sK23)
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_44
| ~ spl329_129 ),
inference(forward_subsumption_resolution,[],[f41783,f26787]) ).
fof(f41808,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ v4_orders_2(sK23)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_44
| ~ spl329_129 ),
inference(forward_subsumption_resolution,[],[f41797,f20637]) ).
fof(f41819,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ v1_lattice3(sK23)
| ~ l1_orders_2(sK23)
| ~ spl329_44
| ~ spl329_129 ),
inference(forward_subsumption_resolution,[],[f41808,f20635]) ).
fof(f41845,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ l1_orders_2(sK23)
| ~ spl329_44
| ~ spl329_129 ),
inference(forward_subsumption_resolution,[],[f41819,f20634]) ).
fof(f41850,plain,
( k13_lattice3(sK22,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ spl329_44
| ~ spl329_129 ),
inference(forward_subsumption_resolution,[],[f41845,f20633]) ).
fof(f43139,plain,
( ~ r1_orders_2(sK22,sK27,k13_lattice3(sK23,sK26,sK27))
| ~ r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| ~ r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ spl329_130 ),
inference(resolution,[],[f41723,f23819]) ).
fof(f43189,plain,
( ~ r1_orders_2(sK22,sK26,k13_lattice3(sK23,sK26,sK27))
| ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| ~ r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ spl329_50
| ~ spl329_130 ),
inference(forward_subsumption_resolution,[],[f43139,f26987]) ).
fof(f43211,plain,
( ~ m1_subset_1(k13_lattice3(sK23,sK26,sK27),u1_struct_0(sK22))
| ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| ~ r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ spl329_50
| ~ spl329_51
| ~ spl329_130 ),
inference(forward_subsumption_resolution,[],[f43189,f26992]) ).
fof(f43230,plain,
( ~ m1_subset_1(k13_lattice3(sK22,sK26,sK27),u1_struct_0(sK23))
| ~ r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ spl329_37
| ~ spl329_50
| ~ spl329_51
| ~ spl329_130 ),
inference(forward_subsumption_resolution,[],[f43211,f26727]) ).
fof(f43249,plain,
( ~ r1_orders_2(sK23,sK27,k13_lattice3(sK22,sK26,sK27))
| k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ spl329_37
| ~ spl329_44
| ~ spl329_50
| ~ spl329_51
| ~ spl329_130 ),
inference(forward_subsumption_resolution,[],[f43230,f26787]) ).
fof(f43268,plain,
( k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK23,k13_lattice3(sK22,sK26,sK27),sK26)
| ~ spl329_37
| ~ spl329_44
| ~ spl329_50
| ~ spl329_51
| ~ spl329_128
| ~ spl329_130 ),
inference(forward_subsumption_resolution,[],[f43249,f41714]) ).
fof(f43273,plain,
( k13_lattice3(sK23,sK26,sK27) = k13_lattice3(sK22,sK26,sK27)
| ~ spl329_37
| ~ spl329_44
| ~ spl329_50
| ~ spl329_51
| ~ spl329_128
| ~ spl329_129
| ~ spl329_130 ),
inference(forward_demodulation,[],[f43268,f41850]) ).
fof(f43274,plain,
( $false
| ~ spl329_37
| ~ spl329_44
| ~ spl329_50
| ~ spl329_51
| ~ spl329_128
| ~ spl329_129
| ~ spl329_130 ),
inference(forward_subsumption_resolution,[],[f43273,f22315]) ).
fof(f43275,plain,
( ~ spl329_37
| ~ spl329_44
| ~ spl329_50
| ~ spl329_51
| ~ spl329_128
| ~ spl329_129
| ~ spl329_130 ),
inference(avatar_contradiction_clause,[],[f43274]) ).
cnf(s7,plain,
( spl329_14
| spl329_15 ),
inference(sat_conversion,[],[f24686]) ).
cnf(s8,plain,
( spl329_16
| spl329_17 ),
inference(sat_conversion,[],[f24695]) ).
cnf(s9,plain,
( spl329_14
| spl329_18 ),
inference(sat_conversion,[],[f24700]) ).
cnf(s10,plain,
( spl329_16
| spl329_19 ),
inference(sat_conversion,[],[f24705]) ).
cnf(s12,plain,
~ spl329_16,
inference(sat_conversion,[],[f24719]) ).
cnf(s14,plain,
~ spl329_14,
inference(sat_conversion,[],[f24730]) ).
cnf(s29,plain,
( ~ spl329_15
| ~ spl329_17
| ~ spl329_18
| ~ spl329_19
| spl329_37 ),
inference(sat_conversion,[],[f26868]) ).
cnf(s40,plain,
( ~ spl329_37
| spl329_50 ),
inference(sat_conversion,[],[f27009]) ).
cnf(s41,plain,
( ~ spl329_37
| spl329_51 ),
inference(sat_conversion,[],[f27010]) ).
cnf(s54,plain,
( spl329_14
| spl329_16
| spl329_31
| ~ spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(sat_conversion,[],[f27327]) ).
cnf(s64,plain,
( ~ spl329_18
| ~ spl329_19
| spl329_35
| ~ spl329_37
| ~ spl329_51 ),
inference(sat_conversion,[],[f27720]) ).
cnf(s130,plain,
( ~ spl329_115
| spl329_117 ),
inference(sat_conversion,[],[f35713]) ).
cnf(s132,plain,
spl329_115,
inference(sat_conversion,[],[f35727]) ).
cnf(s152,plain,
( ~ spl329_15
| ~ spl329_17
| spl329_38
| ~ spl329_115
| ~ spl329_117 ),
inference(sat_conversion,[],[f41560]) ).
cnf(s153,plain,
( ~ spl329_38
| spl329_44 ),
inference(sat_conversion,[],[f41589]) ).
cnf(s158,plain,
( ~ spl329_44
| spl329_128 ),
inference(sat_conversion,[],[f41732]) ).
cnf(s159,plain,
( ~ spl329_44
| spl329_129 ),
inference(sat_conversion,[],[f41733]) ).
cnf(s162,plain,
( ~ spl329_31
| ~ spl329_44
| spl329_130 ),
inference(sat_conversion,[],[f41754]) ).
cnf(s183,plain,
( ~ spl329_37
| ~ spl329_44
| ~ spl329_50
| ~ spl329_51
| ~ spl329_128
| ~ spl329_129
| ~ spl329_130 ),
inference(sat_conversion,[],[f43275]) ).
cnf(s185,plain,
spl329_117,
inference(rat,[],[s130,s132]) ).
cnf(s188,plain,
spl329_19,
inference(rat,[],[s10,s12]) ).
cnf(s189,plain,
spl329_18,
inference(rat,[],[s9,s14]) ).
cnf(s190,plain,
spl329_17,
inference(rat,[],[s8,s12]) ).
cnf(s191,plain,
spl329_15,
inference(rat,[],[s7,s14]) ).
cnf(s192,plain,
spl329_38,
inference(rat,[],[s152,s185,s132,s190,s191]) ).
cnf(s193,plain,
spl329_37,
inference(rat,[],[s29,s190,s188,s189,s191]) ).
cnf(s194,plain,
spl329_44,
inference(rat,[],[s153,s192]) ).
cnf(s195,plain,
spl329_51,
inference(rat,[],[s41,s193]) ).
cnf(s196,plain,
spl329_50,
inference(rat,[],[s40,s193]) ).
cnf(s198,plain,
spl329_35,
inference(rat,[],[s64,s195,s189,s188,s193]) ).
cnf(s199,plain,
spl329_129,
inference(rat,[],[s159,s194]) ).
cnf(s200,plain,
spl329_128,
inference(rat,[],[s158,s194]) ).
cnf(s210,plain,
spl329_31,
inference(rat,[],[s54,s195,s193,s12,s14,s198]) ).
cnf(s213,plain,
~ spl329_130,
inference(rat,[],[s183,s196,s199,s194,s195,s193,s200]) ).
cnf(s226,plain,
$false,
inference(rat,[],[s162,s194,s213,s210]) ).
fof(f43276,plain,
$false,
inference(avatar_sat_refutation,[],[s226]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU410+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 05:15:45 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.44/4.02 % (3476858)Detected formulas, will run a generic FOF schedule.
% 14.44/4.02 % (3476863)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=987637190:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 14.44/4.02 % (3476867)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3937487050:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 14.44/4.02 % (3476864)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=2001010704:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 14.44/4.02 % (3476865)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=3699385523:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 14.44/4.02 % (3476866)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=819296615:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 14.44/4.02 % (3476869)dis-21_1_sil=8000:lcm=predicate:random_seed=1738950847:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 14.44/4.02 % (3476868)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3048515003:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 14.44/4.02 % (3476868)Instruction limit reached!
% 14.44/4.02 % (3476868)------------------------------
% 14.44/4.02 % (3476868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.44/4.02 % (3476868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.44/4.02 % (3476868)CaDiCaL version: 2.1.3
% 14.44/4.02 % (3476868)Termination reason: Instruction limit
% 14.44/4.02 % (3476868)Termination phase: Property scanning
% 14.44/4.02 % (3476868)Time elapsed: 0.061 s
% 14.44/4.02 % (3476868)Peak memory usage: 112 MB
% 14.44/4.02 % (3476868)Instructions burned: 141 (million)
% 14.44/4.02 % (3476866)Instruction limit reached!
% 14.44/4.02 % (3476866)------------------------------
% 14.44/4.02 % (3476866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.44/4.02 % (3476866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.44/4.02 % (3476866)CaDiCaL version: 2.1.3
% 14.44/4.02 % (3476866)Termination reason: Instruction limit
% 14.44/4.02 % (3476866)Termination phase: SInE selection
% 14.44/4.02 % (3476866)Time elapsed: 0.085 s
% 14.44/4.02 % (3476866)Peak memory usage: 112 MB
% 14.44/4.02 % (3476866)Instructions burned: 109 (million)
% 14.44/4.02 % (3476869)Instruction limit reached!
% 14.44/4.02 % (3476869)------------------------------
% 14.44/4.02 % (3476869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.44/4.02 % (3476869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.44/4.02 % (3476869)CaDiCaL version: 2.1.3
% 14.44/4.02 % (3476869)Termination reason: Instruction limit
% 14.44/4.02 % (3476869)Termination phase: SInE selection
% 14.44/4.02 % (3476869)Time elapsed: 0.086 s
% 14.44/4.02 % (3476869)Peak memory usage: 112 MB
% 14.44/4.02 % (3476869)Instructions burned: 129 (million)
% 14.44/4.02 % (3476867)Instruction limit reached!
% 14.44/4.02 % (3476867)------------------------------
% 14.44/4.02 % (3476867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.44/4.02 % (3476867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.44/4.02 % (3476867)CaDiCaL version: 2.1.3
% 14.44/4.02 % (3476867)Termination reason: Instruction limit
% 14.44/4.02 % (3476867)Termination phase: Preprocessing 1
% 14.44/4.02 % (3476867)Time elapsed: 0.102 s
% 14.44/4.02 % (3476867)Peak memory usage: 113 MB
% 14.44/4.02 % (3476867)Instructions burned: 119 (million)
% 14.44/4.02 % (3476877)lrs+10_1_sil=8000:sp=occurrence:random_seed=3472280159:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 14.44/4.02 % (3476878)lrs+10_1_sil=32000:urr=on:br=off:random_seed=454413640:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 14.44/4.02 % (3476879)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1808812007:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 14.44/4.02 % (3476880)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=2032545112:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 14.44/4.02 % (3476878)Instruction limit reached!
% 23.29/5.04 % (3476878)------------------------------
% 23.29/5.04 % (3476878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.04 % (3476878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.04 % (3476878)CaDiCaL version: 2.1.3
% 23.29/5.04 % (3476878)Termination reason: Instruction limit
% 23.29/5.04 % (3476878)Termination phase: Property scanning
% 23.29/5.04 % (3476878)Time elapsed: 0.069 s
% 23.29/5.04 % (3476878)Peak memory usage: 112 MB
% 23.29/5.04 % (3476878)Instructions burned: 159 (million)
% 23.29/5.04 % (3476880)Instruction limit reached!
% 23.29/5.04 % (3476880)------------------------------
% 23.29/5.04 % (3476880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.04 % (3476880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.04 % (3476880)CaDiCaL version: 2.1.3
% 23.29/5.04 % (3476880)Termination reason: Instruction limit
% 23.29/5.04 % (3476880)Termination phase: Property scanning
% 23.29/5.04 % (3476880)Time elapsed: 0.107 s
% 23.29/5.04 % (3476880)Peak memory usage: 112 MB
% 23.29/5.04 % (3476880)Instructions burned: 248 (million)
% 23.29/5.04 % (3476877)Instruction limit reached!
% 23.29/5.04 % (3476877)------------------------------
% 23.29/5.04 % (3476877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.04 % (3476877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.04 % (3476877)CaDiCaL version: 2.1.3
% 23.29/5.04 % (3476877)Termination reason: Instruction limit
% 23.29/5.04 % (3476877)Termination phase: Saturation
% 23.29/5.04 % (3476877)Time elapsed: 0.204 s
% 23.29/5.04 % (3476877)Peak memory usage: 120 MB
% 23.29/5.04 % (3476877)Instructions burned: 286 (million)
% 23.29/5.04 % (3476885)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2384187625:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 23.29/5.04 % (3476879)Instruction limit reached!
% 23.29/5.04 % (3476879)------------------------------
% 23.29/5.04 % (3476879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.04 % (3476879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.04 % (3476879)CaDiCaL version: 2.1.3
% 23.29/5.04 % (3476879)Termination reason: Instruction limit
% 23.29/5.04 % (3476879)Termination phase: Saturation
% 23.29/5.04 % (3476879)Time elapsed: 0.244 s
% 23.29/5.04 % (3476879)Peak memory usage: 119 MB
% 23.29/5.04 % (3476879)Instructions burned: 325 (million)
% 23.29/5.04 % (3476886)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3403040353:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 23.29/5.04 % (3476887)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1391780097:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 23.29/5.04 % (3476887)Instruction limit reached!
% 23.29/5.04 % (3476887)------------------------------
% 23.29/5.04 % (3476887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.04 % (3476887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.04 % (3476887)CaDiCaL version: 2.1.3
% 23.29/5.04 % (3476887)Termination reason: Instruction limit
% 23.29/5.04 % (3476887)Termination phase: SInE selection
% 23.29/5.04 % (3476887)Time elapsed: 0.089 s
% 23.29/5.04 % (3476887)Peak memory usage: 112 MB
% 23.29/5.04 % (3476887)Instructions burned: 113 (million)
% 23.29/5.04 % (3476890)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1147145459:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 23.29/5.04 % (3476885)Instruction limit reached!
% 23.29/5.04 % (3476885)------------------------------
% 23.29/5.04 % (3476885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.04 % (3476885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.04 % (3476885)CaDiCaL version: 2.1.3
% 23.29/5.04 % (3476885)Termination reason: Instruction limit
% 23.29/5.04 % (3476885)Termination phase: Preprocessing 3
% 23.29/5.04 % (3476885)Time elapsed: 0.222 s
% 23.29/5.04 % (3476885)Peak memory usage: 119 MB
% 23.29/5.04 % (3476885)Instructions burned: 295 (million)
% 23.29/5.04 % (3476890)Instruction limit reached!
% 23.29/5.04 % (3476890)------------------------------
% 23.29/5.04 % (3476890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.04 % (3476890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.04 % (3476890)CaDiCaL version: 2.1.3
% 50.72/9.02 % (3476890)Termination reason: Instruction limit
% 50.72/9.02 % (3476890)Termination phase: Preprocessing 1
% 50.72/9.02 % (3476890)Time elapsed: 0.093 s
% 50.72/9.02 % (3476890)Peak memory usage: 113 MB
% 50.72/9.02 % (3476890)Instructions burned: 128 (million)
% 50.72/9.02 % (3476893)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=999366606:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2981 on theBenchmark for (2981ds/114Mi)
% 50.72/9.02 % (3476894)lrs+10_1_sil=8000:sp=occurrence:random_seed=4092188475:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2981 on theBenchmark for (2981ds/907Mi)
% 50.72/9.02 % (3476893)Instruction limit reached!
% 50.72/9.02 % (3476893)------------------------------
% 50.72/9.02 % (3476893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.72/9.02 % (3476893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.72/9.02 % (3476893)CaDiCaL version: 2.1.3
% 50.72/9.02 % (3476893)Termination reason: Instruction limit
% 50.72/9.02 % (3476893)Termination phase: Property scanning
% 50.72/9.02 % (3476893)Time elapsed: 0.051 s
% 50.72/9.02 % (3476893)Peak memory usage: 112 MB
% 50.72/9.02 % (3476893)Instructions burned: 117 (million)
% 50.72/9.02 % (3476895)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2363586002:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 50.72/9.02 % (3476898)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1878148917:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 50.72/9.02 % (3476895)Instruction limit reached!
% 50.72/9.02 % (3476895)------------------------------
% 50.72/9.02 % (3476895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.72/9.02 % (3476895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.72/9.02 % (3476895)CaDiCaL version: 2.1.3
% 50.72/9.02 % (3476895)Termination reason: Instruction limit
% 50.72/9.02 % (3476895)Termination phase: Saturation
% 50.72/9.02 % (3476895)Time elapsed: 0.300 s
% 50.72/9.02 % (3476895)Peak memory usage: 120 MB
% 50.72/9.02 % (3476895)Instructions burned: 438 (million)
% 50.72/9.02 % (3476901)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2865770186:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 50.72/9.02 % (3476894)Instruction limit reached!
% 50.72/9.02 % (3476894)------------------------------
% 50.72/9.02 % (3476894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.72/9.02 % (3476894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.72/9.02 % (3476894)CaDiCaL version: 2.1.3
% 50.72/9.02 % (3476894)Termination reason: Instruction limit
% 50.72/9.02 % (3476894)Termination phase: Saturation
% 50.72/9.02 % (3476894)Time elapsed: 0.546 s
% 50.72/9.02 % (3476894)Peak memory usage: 130 MB
% 50.72/9.02 % (3476894)Instructions burned: 909 (million)
% 50.72/9.02 % (3476901)Instruction limit reached!
% 50.72/9.02 % (3476901)------------------------------
% 50.72/9.02 % (3476901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.72/9.02 % (3476901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.72/9.02 % (3476901)CaDiCaL version: 2.1.3
% 50.72/9.02 % (3476901)Termination reason: Instruction limit
% 50.72/9.02 % (3476901)Termination phase: NewCNF
% 50.72/9.02 % (3476901)Time elapsed: 0.117 s
% 50.72/9.02 % (3476901)Peak memory usage: 115 MB
% 50.72/9.02 % (3476901)Instructions burned: 135 (million)
% 50.72/9.02 % (3476903)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3288706606:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi)
% 50.72/9.02 % (3476904)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=676879098:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 50.72/9.02 % (3476886)Instruction limit reached!
% 50.72/9.02 % (3476886)------------------------------
% 50.72/9.02 % (3476886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.72/9.02 % (3476886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.72/9.02 % (3476886)CaDiCaL version: 2.1.3
% 50.72/9.02 % (3476886)Termination reason: Instruction limit
% 50.72/9.02 % (3476886)Termination phase: Property scanning
% 50.72/9.02 % (3476886)Time elapsed: 1.257 s
% 50.72/9.02 % (3476886)Peak memory usage: 171 MB
% 50.72/9.02 % (3476886)Instructions burned: 2351 (million)
% 50.72/9.02 % (3476907)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=669008421:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 91.20/14.62 % (3476903)Instruction limit reached!
% 91.20/14.62 % (3476903)------------------------------
% 91.20/14.62 % (3476903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.20/14.62 % (3476903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.20/14.62 % (3476903)CaDiCaL version: 2.1.3
% 91.20/14.62 % (3476903)Termination reason: Instruction limit
% 91.20/14.62 % (3476903)Termination phase: Preprocessing 3
% 91.20/14.62 % (3476903)Time elapsed: 0.473 s
% 91.20/14.62 % (3476903)Peak memory usage: 135 MB
% 91.20/14.62 % (3476903)Instructions burned: 593 (million)
% 91.20/14.62 % (3476907)Instruction limit reached!
% 91.20/14.62 % (3476907)------------------------------
% 91.20/14.62 % (3476907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.20/14.62 % (3476907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.20/14.62 % (3476907)CaDiCaL version: 2.1.3
% 91.20/14.62 % (3476907)Termination reason: Instruction limit
% 91.20/14.62 % (3476907)Termination phase: Property scanning
% 91.20/14.62 % (3476907)Time elapsed: 0.057 s
% 91.20/14.62 % (3476907)Peak memory usage: 112 MB
% 91.20/14.62 % (3476907)Instructions burned: 126 (million)
% 91.20/14.62 % (3476910)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2897560668:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/141Mi)
% 91.20/14.62 % (3476909)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2622441102:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 91.20/14.62 % (3476909)Instruction limit reached!
% 91.20/14.62 % (3476909)------------------------------
% 91.20/14.62 % (3476909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.20/14.62 % (3476909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.20/14.62 % (3476909)CaDiCaL version: 2.1.3
% 91.20/14.62 % (3476909)Termination reason: Instruction limit
% 91.20/14.62 % (3476909)Termination phase: Property scanning
% 91.20/14.62 % (3476909)Time elapsed: 0.060 s
% 91.20/14.62 % (3476909)Peak memory usage: 112 MB
% 91.20/14.62 % (3476909)Instructions burned: 136 (million)
% 91.20/14.62 % (3476910)Instruction limit reached!
% 91.20/14.62 % (3476910)------------------------------
% 91.20/14.62 % (3476910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.20/14.62 % (3476910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.20/14.62 % (3476910)CaDiCaL version: 2.1.3
% 91.20/14.62 % (3476910)Termination reason: Instruction limit
% 91.20/14.62 % (3476910)Termination phase: Saturation
% 91.20/14.62 % (3476910)Time elapsed: 0.118 s
% 91.20/14.62 % (3476910)Peak memory usage: 117 MB
% 91.20/14.62 % (3476910)Instructions burned: 141 (million)
% 91.20/14.62 % (3476913)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=997531145:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2965 on theBenchmark for (2965ds/431Mi)
% 91.20/14.62 % (3476914)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=817169110:i=6060:aac=none:ins=25_2965 on theBenchmark for (2965ds/6060Mi)
% 91.20/14.62 % (3476913)Refutation not found, incomplete strategy
% 91.20/14.62 % (3476913)------------------------------
% 91.20/14.62 % (3476913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.20/14.62 % (3476913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.20/14.62 % (3476913)CaDiCaL version: 2.1.3
% 91.20/14.62 % (3476913)Termination reason: Refutation not found, incomplete strategy
% 91.20/14.62 % (3476913)Time elapsed: 0.114 s
% 91.20/14.62 % (3476913)Peak memory usage: 118 MB
% 91.20/14.62 % (3476913)Instructions burned: 132 (million)
% 91.20/14.62 % (3476913)------------------------------
% 91.20/14.62 % (3476913)------------------------------
% 91.20/14.62 % (3476917)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=4114312965:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2960 on theBenchmark for (2960ds/150Mi)
% 91.20/14.62 % (3476917)Instruction limit reached!
% 91.20/14.62 % (3476917)------------------------------
% 91.20/14.62 % (3476917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.20/14.62 % (3476917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476917)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476917)Termination reason: Instruction limit
% 46.94/16.07 % (3476917)Termination phase: Preprocessing 1
% 46.94/16.07 % (3476917)Time elapsed: 0.123 s
% 46.94/16.07 % (3476917)Peak memory usage: 113 MB
% 46.94/16.07 % (3476917)Instructions burned: 151 (million)
% 46.94/16.07 % (3476919)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1020420825:i=14155:bd=all_2958 on theBenchmark for (2958ds/14155Mi)
% 46.94/16.07 % (3476898)Instruction limit reached!
% 46.94/16.07 % (3476898)------------------------------
% 46.94/16.07 % (3476898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476898)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476898)Termination reason: Instruction limit
% 46.94/16.07 % (3476898)Termination phase: Saturation
% 46.94/16.07 % (3476898)Time elapsed: 2.458 s
% 46.94/16.07 % (3476898)Peak memory usage: 186 MB
% 46.94/16.07 % (3476898)Instructions burned: 5202 (million)
% 46.94/16.07 % (3476921)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=304876593:i=667:av=off:fsr=off_2953 on theBenchmark for (2953ds/667Mi)
% 46.94/16.07 % (3476921)Instruction limit reached!
% 46.94/16.07 % (3476921)------------------------------
% 46.94/16.07 % (3476921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476921)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476921)Termination reason: Instruction limit
% 46.94/16.07 % (3476921)Termination phase: NewCNF
% 46.94/16.07 % (3476921)Time elapsed: 0.520 s
% 46.94/16.07 % (3476921)Peak memory usage: 149 MB
% 46.94/16.07 % (3476921)Instructions burned: 669 (million)
% 46.94/16.07 % (3476923)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=2521923556:s2a=on:i=185:s2at=1.8:fdi=4_2946 on theBenchmark for (2946ds/185Mi)
% 46.94/16.07 % (3476923)Instruction limit reached!
% 46.94/16.07 % (3476923)------------------------------
% 46.94/16.07 % (3476923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476923)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476923)Termination reason: Instruction limit
% 46.94/16.07 % (3476923)Termination phase: SInE selection
% 46.94/16.07 % (3476923)Time elapsed: 0.143 s
% 46.94/16.07 % (3476923)Peak memory usage: 113 MB
% 46.94/16.07 % (3476923)Instructions burned: 185 (million)
% 46.94/16.07 % (3476925)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=27303617:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2943 on theBenchmark for (2943ds/193Mi)
% 46.94/16.07 % (3476925)Instruction limit reached!
% 46.94/16.07 % (3476925)------------------------------
% 46.94/16.07 % (3476925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476925)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476925)Termination reason: Instruction limit
% 46.94/16.07 % (3476925)Termination phase: SInE selection
% 46.94/16.07 % (3476925)Time elapsed: 0.158 s
% 46.94/16.07 % (3476925)Peak memory usage: 112 MB
% 46.94/16.07 % (3476925)Instructions burned: 194 (million)
% 46.94/16.07 % (3476927)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3836263048:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2940 on theBenchmark for (2940ds/4850Mi)
% 46.94/16.07 % (3476914)Instruction limit reached!
% 46.94/16.07 % (3476914)------------------------------
% 46.94/16.07 % (3476914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476914)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476914)Termination reason: Instruction limit
% 46.94/16.07 % (3476914)Termination phase: Saturation
% 46.94/16.07 % (3476914)Time elapsed: 4.536 s
% 46.94/16.07 % (3476914)Peak memory usage: 580 MB
% 46.94/16.07 % (3476914)Instructions burned: 6060 (million)
% 46.94/16.07 % (3476927)Instruction limit reached!
% 46.94/16.07 % (3476927)------------------------------
% 46.94/16.07 % (3476927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476927)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476927)Termination reason: Instruction limit
% 46.94/16.07 % (3476927)Termination phase: Function definition elimination
% 46.94/16.07 % (3476927)Time elapsed: 2.115 s
% 46.94/16.07 % (3476927)Peak memory usage: 157 MB
% 46.94/16.07 % (3476927)Instructions burned: 4850 (million)
% 46.94/16.07 % (3476929)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1463641932:i=12111:sd=1:ss=included_2918 on theBenchmark for (2918ds/12111Mi)
% 46.94/16.07 % (3476930)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2950252369:i=319:kws=precedence:fsr=off_2917 on theBenchmark for (2917ds/319Mi)
% 46.94/16.07 % (3476930)Instruction limit reached!
% 46.94/16.07 % (3476930)------------------------------
% 46.94/16.07 % (3476930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476930)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476930)Termination reason: Instruction limit
% 46.94/16.07 % (3476930)Termination phase: Naming
% 46.94/16.07 % (3476930)Time elapsed: 0.258 s
% 46.94/16.07 % (3476930)Peak memory usage: 135 MB
% 46.94/16.07 % (3476930)Instructions burned: 320 (million)
% 46.94/16.07 % (3476933)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3886560649:i=2064:ep=RST_2913 on theBenchmark for (2913ds/2064Mi)
% 46.94/16.07 % (3476933)Instruction limit reached!
% 46.94/16.07 % (3476933)------------------------------
% 46.94/16.07 % (3476933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476933)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476933)Termination reason: Instruction limit
% 46.94/16.07 % (3476933)Termination phase: Property scanning
% 46.94/16.07 % (3476933)Time elapsed: 1.118 s
% 46.94/16.07 % (3476933)Peak memory usage: 171 MB
% 46.94/16.07 % (3476933)Instructions burned: 2066 (million)
% 46.94/16.07 % (3476935)dis-1011_128_sil=32000:random_seed=2304749921:i=3706:ep=RST:av=off_2901 on theBenchmark for (2901ds/3706Mi)
% 46.94/16.07 % (3476904)Instruction limit reached!
% 46.94/16.07 % (3476904)------------------------------
% 46.94/16.07 % (3476904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476904)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476904)Termination reason: Instruction limit
% 46.94/16.07 % (3476904)Termination phase: Saturation
% 46.94/16.07 % (3476904)Time elapsed: 7.849 s
% 46.94/16.07 % (3476904)Peak memory usage: 282 MB
% 46.94/16.07 % (3476904)Instructions burned: 13194 (million)
% 46.94/16.07 % (3476937)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1547384142:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2893 on theBenchmark for (2893ds/757Mi)
% 46.94/16.07 % (3476937)Instruction limit reached!
% 46.94/16.07 % (3476937)------------------------------
% 46.94/16.07 % (3476937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476937)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476937)Termination reason: Instruction limit
% 46.94/16.07 % (3476937)Termination phase: Saturation
% 46.94/16.07 % (3476937)Time elapsed: 0.472 s
% 46.94/16.07 % (3476937)Peak memory usage: 126 MB
% 46.94/16.07 % (3476937)Instructions burned: 757 (million)
% 46.94/16.07 % (3476939)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1029390407:i=13913:ss=axioms:sgt=8_2886 on theBenchmark for (2886ds/13913Mi)
% 46.94/16.07 % (3476935)Instruction limit reached!
% 46.94/16.07 % (3476935)------------------------------
% 46.94/16.07 % (3476935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476935)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476935)Termination reason: Instruction limit
% 46.94/16.07 % (3476935)Termination phase: Saturation
% 46.94/16.07 % (3476935)Time elapsed: 1.860 s
% 46.94/16.07 % (3476935)Peak memory usage: 187 MB
% 46.94/16.07 % (3476935)Instructions burned: 3706 (million)
% 46.94/16.07 % (3476941)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3690037462:i=9925:aac=none_2880 on theBenchmark for (2880ds/9925Mi)
% 46.94/16.07 % (3476919)Instruction limit reached!
% 46.94/16.07 % (3476919)------------------------------
% 46.94/16.07 % (3476919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.94/16.07 % (3476919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.94/16.07 % (3476919)CaDiCaL version: 2.1.3
% 46.94/16.07 % (3476919)Termination reason: Instruction limit
% 46.94/16.07 % (3476919)Termination phase: Saturation
% 46.94/16.07 % (3476919)Time elapsed: 9.438 s
% 46.94/16.07 % (3476919)Peak memory usage: 521 MB
% 46.94/16.07 % (3476919)Instructions burned: 14155 (million)
% 46.94/16.07 % (3476943)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1593200164:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2861 on theBenchmark for (2861ds/2479Mi)
% 46.94/16.07 % (3476939)First to succeed.
% 46.94/16.07 % (3476939)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3476858"
% 46.94/16.07 % (3476939)Refutation found. Thanks to Tanya!
% 46.94/16.07 % SZS status Theorem for theBenchmark
% 46.94/16.07 % SZS output start Proof for theBenchmark
% See solution above
% 101.65/16.30 % (3476939)------------------------------
% 101.65/16.30 % (3476939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.65/16.30 % (3476939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.65/16.30 % (3476939)CaDiCaL version: 2.1.3
% 101.65/16.30 % (3476939)Termination reason: Refutation
% 101.65/16.30 % (3476939)Time elapsed: 3.436 s
% 101.65/16.30 % (3476939)Peak memory usage: 188 MB
% 101.65/16.30 % (3476939)Instructions burned: 5599 (million)
% 101.65/16.30 % (3476939)------------------------------
% 101.65/16.30 % (3476939)------------------------------
% 101.65/16.30 % (3476858)Success in time 15.215 s
% 101.65/16.30 % Vampire exiting
%------------------------------------------------------------------------------