%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT309+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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:46 AM UTC 2026
% Result : Theorem 25.46s 7.58s
% Output : Refutation 43.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 43
% Syntax : Number of formulae : 343 ( 41 unt; 17 def)
% Number of atoms : 1450 ( 166 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 1862 ( 755 ~; 878 |; 144 &)
% ( 31 <=>; 54 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 18 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 2 con; 0-3 aty)
% Number of variables : 322 ( 0 sgn 314 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f6728,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r3_lattices(X0,X1,k6_lattices(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_lattices) ).
fof(f8589,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_0(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f8592,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_filter_0) ).
fof(f8608,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0)
& r2_hidden(k5_lattices(X0),X1) )
=> ( X1 = k1_filter_0(X0)
& X1 = u1_struct_0(X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t32_filter_0) ).
fof(f8676,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_filter_0(k2_filter_0(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_filter_0) ).
fof(f9358,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f9363,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9391,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f9428,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
=> ( ( X1 = X3
& X2 = X4 )
=> r3_lattices(k1_lattice2(X0),X4,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t53_lattice2) ).
fof(f9439,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t64_lattice2) ).
fof(f9454,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> k6_lattices(X0) = k5_lattices(k1_lattice2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t79_lattice2) ).
fof(f9463,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f10110,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( k2_filter_0(X0,X1) = k2_filter_0(X0,X2)
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_filter_1) ).
fof(f13531,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f13540,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k2_filter_2(X0,X1) = k2_filter_0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f13595,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f13600,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f13608,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v13_lattices(X0)
=> r2_hidden(k5_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_filter_2) ).
fof(f13611,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_filter_2(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t28_filter_2) ).
fof(f13612,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k17_filter_2(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f13615,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_filter_2) ).
fof(f13616,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_filter_2) ).
fof(f13620,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ~ ( X1 != u1_struct_0(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ~ ( r1_tarski(X1,X2)
& r2_filter_2(X0,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_filter_2) ).
fof(f13622,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ~ ( v14_lattices(X0)
& X1 != k6_lattices(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ~ ( r2_hidden(X1,X2)
& r2_filter_2(X0,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_filter_2) ).
fof(f13623,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ~ ( v14_lattices(X0)
& X1 != k6_lattices(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ~ ( r2_hidden(X1,X2)
& r2_filter_2(X0,X2) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13622]) ).
fof(f13670,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13531]) ).
fof(f13671,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13670]) ).
fof(f13688,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f13540]) ).
fof(f13689,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13688]) ).
fof(f13795,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13595]) ).
fof(f13796,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13795]) ).
fof(f13805,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13600]) ).
fof(f13806,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13805]) ).
fof(f13821,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k5_lattices(X0),X1)
| ~ v13_lattices(X0)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13608]) ).
fof(f13822,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k5_lattices(X0),X1)
| ~ v13_lattices(X0)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13821]) ).
fof(f13827,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13611]) ).
fof(f13828,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13827]) ).
fof(f13829,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13612]) ).
fof(f13830,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13829]) ).
fof(f13835,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13615]) ).
fof(f13836,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13835]) ).
fof(f13837,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13616]) ).
fof(f13838,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13837]) ).
fof(f13845,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ? [X2] :
( r1_tarski(X1,X2)
& r2_filter_2(X0,X2)
& m2_filter_2(X2,X0) )
| ~ m2_filter_2(X1,X0) )
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13620]) ).
fof(f13846,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ? [X2] :
( r1_tarski(X1,X2)
& r2_filter_2(X0,X2)
& m2_filter_2(X2,X0) )
| ~ m2_filter_2(X1,X0) )
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13845]) ).
fof(f13849,plain,
? [X0] :
( ? [X1] :
( v14_lattices(X0)
& X1 != k6_lattices(X0)
& ! [X2] :
( ~ r2_hidden(X1,X2)
| ~ r2_filter_2(X0,X2)
| ~ m2_filter_2(X2,X0) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13623]) ).
fof(f13850,plain,
? [X0] :
( ? [X1] :
( v14_lattices(X0)
& X1 != k6_lattices(X0)
& ! [X2] :
( ~ r2_hidden(X1,X2)
| ~ r2_filter_2(X0,X2)
| ~ m2_filter_2(X2,X0) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f13849]) ).
fof(f13897,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_filter_0(X0)
& X1 = u1_struct_0(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8608]) ).
fof(f13898,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_filter_0(X0)
& X1 = u1_struct_0(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13897]) ).
fof(f13903,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8589]) ).
fof(f13904,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13903]) ).
fof(f13905,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| k2_filter_0(X0,X2) != k2_filter_0(X0,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f10110]) ).
fof(f13906,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| k2_filter_0(X0,X2) != k2_filter_0(X0,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13905]) ).
fof(f13907,plain,
! [X0,X1] :
( m1_filter_0(k2_filter_0(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f8676]) ).
fof(f13908,plain,
! [X0,X1] :
( m1_filter_0(k2_filter_0(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13907]) ).
fof(f13913,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8592]) ).
fof(f13914,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13913]) ).
fof(f13959,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9439]) ).
fof(f13960,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13959]) ).
fof(f13965,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( r3_lattices(k1_lattice2(X0),X4,X3)
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0))) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9428]) ).
fof(f13966,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( r3_lattices(k1_lattice2(X0),X4,X3)
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0))) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13965]) ).
fof(f13969,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9391]) ).
fof(f13970,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13969]) ).
fof(f13982,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f13985,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9363]) ).
fof(f13986,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13985]) ).
fof(f13987,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f13988,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13987]) ).
fof(f14157,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f14217,plain,
! [X0] :
( k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9454]) ).
fof(f14218,plain,
! [X0] :
( k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14217]) ).
fof(f14231,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,X1,k6_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6728]) ).
fof(f14232,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,X1,k6_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14231]) ).
fof(f14341,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f18179,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13671]) ).
fof(f18199,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13806]) ).
fof(f18214,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ( r1_tarski(X1,sK35(X0,X1))
& r2_filter_2(X0,sK35(X0,X1))
& m2_filter_2(sK35(X0,X1),X0) )
| ~ m2_filter_2(X1,X0) )
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(X2,sK35(X0,X1))],[f13846]) ).
fof(f18215,plain,
( v14_lattices(sK36)
& sK37 != k6_lattices(sK36)
& ! [X2] :
( ~ r2_hidden(sK37,X2)
| ~ r2_filter_2(sK36,X2)
| ~ m2_filter_2(X2,sK36) )
& m1_subset_1(sK37,u1_struct_0(sK36))
& ~ v3_struct_0(sK36)
& v10_lattices(sK36)
& l3_lattices(sK36) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37]),skolemize(X0,sK36),skolemize(X1,sK37)],[f13850]) ).
fof(f18239,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X1,k2_filter_0(X0,X2))
| ~ r3_lattices(X0,X2,X1) )
& ( r3_lattices(X0,X2,X1)
| ~ r2_hidden(X1,k2_filter_0(X0,X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13914]) ).
fof(f18249,plain,
! [X0] :
( ( ( v14_lattices(X0)
| ~ v13_lattices(k1_lattice2(X0)) )
& ( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13960]) ).
fof(f18428,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f14341]) ).
fof(f18429,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f18428]) ).
fof(f18430,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK150(X0,X1),X1)
& r2_hidden(sK150(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK150]),skolemize(X2,sK150(X0,X1))],[f18429]) ).
fof(f19654,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18179]) ).
fof(f19665,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| k2_filter_0(X0,X1) = k2_filter_2(X0,X1)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13689]) ).
fof(f19754,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k5_filter_2(X0,X1) = X1
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13796]) ).
fof(f19767,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,k1_lattice2(X0))
| m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18199]) ).
fof(f19789,plain,
! [X0,X1] :
( ~ v13_lattices(X0)
| r2_hidden(k5_lattices(X0),X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13822]) ).
fof(f19792,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_filter_2(u1_struct_0(X0),X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13828]) ).
fof(f19793,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k17_filter_2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13830]) ).
fof(f19798,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13836]) ).
fof(f19801,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| r2_hidden(X1,k18_filter_2(X0,X1))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13838]) ).
fof(f19811,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| m2_filter_2(sK35(X0,X1),X0)
| ~ m2_filter_2(X1,X0)
| u1_struct_0(X0) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18214]) ).
fof(f19812,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| r2_filter_2(X0,sK35(X0,X1))
| u1_struct_0(X0) = X1
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18214]) ).
fof(f19813,plain,
! [X0,X1] :
( r1_tarski(X1,sK35(X0,X1))
| u1_struct_0(X0) = X1
| ~ m2_filter_2(X1,X0)
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18214]) ).
fof(f19815,plain,
l3_lattices(sK36),
inference(cnf_transformation,[],[f18215]) ).
fof(f19816,plain,
v10_lattices(sK36),
inference(cnf_transformation,[],[f18215]) ).
fof(f19817,plain,
~ v3_struct_0(sK36),
inference(cnf_transformation,[],[f18215]) ).
fof(f19818,plain,
m1_subset_1(sK37,u1_struct_0(sK36)),
inference(cnf_transformation,[],[f18215]) ).
fof(f19819,plain,
! [X2] :
( ~ r2_filter_2(sK36,X2)
| ~ r2_hidden(sK37,X2)
| ~ m2_filter_2(X2,sK36) ),
inference(cnf_transformation,[],[f18215]) ).
fof(f19820,plain,
sK37 != k6_lattices(sK36),
inference(cnf_transformation,[],[f18215]) ).
fof(f19821,plain,
v14_lattices(sK36),
inference(cnf_transformation,[],[f18215]) ).
fof(f19875,plain,
! [X0,X1] :
( u1_struct_0(X0) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13898]) ).
fof(f19880,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13904]) ).
fof(f19881,plain,
! [X2,X0,X1] :
( k2_filter_0(X0,X2) != k2_filter_0(X0,X1)
| X1 = X2
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13906]) ).
fof(f19882,plain,
! [X0,X1] :
( m1_filter_0(k2_filter_0(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13908]) ).
fof(f19888,plain,
! [X2,X0,X1] :
( r2_hidden(X1,k2_filter_0(X0,X2))
| ~ r3_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18239]) ).
fof(f19933,plain,
! [X0] :
( ~ v14_lattices(X0)
| v13_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18249]) ).
fof(f19938,plain,
! [X2,X3,X0,X1,X4] :
( r3_lattices(k1_lattice2(X0),X4,X3)
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13966]) ).
fof(f19943,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f13970]) ).
fof(f19965,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13982]) ).
fof(f19968,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13986]) ).
fof(f19978,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13988]) ).
fof(f20207,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f14157]) ).
fof(f20286,plain,
! [X0] :
( ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14218]) ).
fof(f20295,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| r3_lattices(X0,X1,k6_lattices(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14232]) ).
fof(f20496,plain,
! [X3,X0,X1] :
( ~ r1_tarski(X0,X1)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) ),
inference(cnf_transformation,[],[f18430]) ).
fof(f27057,plain,
! [X2,X3,X0,X4] :
( r3_lattices(k1_lattice2(X0),X4,X3)
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
| ~ r3_lattices(X0,X3,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f19938]) ).
fof(f27058,plain,
! [X3,X0,X4] :
( ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
| r3_lattices(k1_lattice2(X0),X4,X3)
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
| ~ r3_lattices(X0,X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f27057]) ).
fof(f27669,plain,
! [X0,X1] :
( ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| u1_struct_0(X0) = X1
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0) ),
inference(duplicate_literal_removal,[],[f19875]) ).
fof(f28528,plain,
( v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| k6_lattices(sK36) = k5_lattices(k1_lattice2(sK36))
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f20286,f19821]) ).
fof(f28529,plain,
( ~ v10_lattices(sK36)
| k6_lattices(sK36) = k5_lattices(k1_lattice2(sK36))
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28528,f19817]) ).
fof(f28530,plain,
( k6_lattices(sK36) = k5_lattices(k1_lattice2(sK36))
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28529,f19816]) ).
fof(f28531,plain,
k6_lattices(sK36) = k5_lattices(k1_lattice2(sK36)),
inference(forward_subsumption_resolution,[],[f28530,f19815]) ).
fof(f28532,plain,
( v3_struct_0(sK36)
| u1_struct_0(sK36) = k17_filter_2(sK36)
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f19793,f19816]) ).
fof(f28533,plain,
( u1_struct_0(sK36) = k17_filter_2(sK36)
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28532,f19817]) ).
fof(f28534,plain,
u1_struct_0(sK36) = k17_filter_2(sK36),
inference(forward_subsumption_resolution,[],[f28533,f19815]) ).
fof(f28536,plain,
( v3_struct_0(sK36)
| u1_struct_0(sK36) = k1_filter_0(sK36)
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f19880,f19816]) ).
fof(f28537,plain,
( u1_struct_0(sK36) = k1_filter_0(sK36)
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28536,f19817]) ).
fof(f28538,plain,
u1_struct_0(sK36) = k1_filter_0(sK36),
inference(forward_subsumption_resolution,[],[f28537,f19815]) ).
fof(f28540,plain,
k17_filter_2(sK36) = k1_filter_0(sK36),
inference(superposition,[],[f28534,f28538]) ).
fof(f28541,plain,
m1_subset_1(sK37,k1_filter_0(sK36)),
inference(superposition,[],[f19818,f28538]) ).
fof(f28548,plain,
! [X0] :
( m2_filter_2(sK35(sK36,X0),sK36)
| ~ m2_filter_2(X0,sK36)
| u1_struct_0(sK36) = X0
| v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f19811,f19821]) ).
fof(f28549,plain,
! [X0] :
( m2_filter_2(sK35(sK36,X0),sK36)
| ~ m2_filter_2(X0,sK36)
| u1_struct_0(sK36) = X0
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28548,f19817]) ).
fof(f28550,plain,
! [X0] :
( m2_filter_2(sK35(sK36,X0),sK36)
| ~ m2_filter_2(X0,sK36)
| u1_struct_0(sK36) = X0
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28549,f19816]) ).
fof(f28551,plain,
! [X0] :
( m2_filter_2(sK35(sK36,X0),sK36)
| ~ m2_filter_2(X0,sK36)
| u1_struct_0(sK36) = X0 ),
inference(forward_subsumption_resolution,[],[f28550,f19815]) ).
fof(f28552,plain,
! [X0] :
( k17_filter_2(sK36) = X0
| m2_filter_2(sK35(sK36,X0),sK36)
| ~ m2_filter_2(X0,sK36) ),
inference(forward_demodulation,[],[f28551,f28534]) ).
fof(f28553,plain,
! [X0] :
( m2_filter_2(sK35(sK36,X0),sK36)
| k1_filter_0(sK36) = X0
| ~ m2_filter_2(X0,sK36) ),
inference(forward_demodulation,[],[f28552,f28540]) ).
fof(f28554,plain,
( v3_struct_0(sK36)
| u1_struct_0(sK36) = u1_struct_0(k1_lattice2(sK36)) ),
inference(resolution,[],[f19943,f19815]) ).
fof(f28555,plain,
u1_struct_0(sK36) = u1_struct_0(k1_lattice2(sK36)),
inference(forward_subsumption_resolution,[],[f28554,f19817]) ).
fof(f28556,plain,
k17_filter_2(sK36) = u1_struct_0(k1_lattice2(sK36)),
inference(forward_demodulation,[],[f28555,f28534]) ).
fof(f28557,plain,
k1_filter_0(sK36) = u1_struct_0(k1_lattice2(sK36)),
inference(forward_demodulation,[],[f28556,f28540]) ).
fof(f28644,plain,
( v3_struct_0(sK36)
| v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f19968,f19816]) ).
fof(f28645,plain,
( v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28644,f19817]) ).
fof(f28646,plain,
v10_lattices(k1_lattice2(sK36)),
inference(forward_subsumption_resolution,[],[f28645,f19815]) ).
fof(f28647,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK36))
| k2_filter_0(k1_lattice2(sK36),X0) = k2_filter_2(k1_lattice2(sK36),X0)
| ~ l3_lattices(k1_lattice2(sK36))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK36))) ),
inference(resolution,[],[f28646,f19665]) ).
fof(f28649,plain,
( v3_struct_0(k1_lattice2(sK36))
| m2_filter_2(u1_struct_0(k1_lattice2(sK36)),k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) ),
inference(resolution,[],[f28646,f19792]) ).
fof(f28657,definition,
( spl865_47
<=> l3_lattices(k1_lattice2(sK36)) ),
introduced(definition,[new_symbols(definition,[spl865_47])],[avatar_definition]) ).
fof(f28658,plain,
( ~ l3_lattices(k1_lattice2(sK36))
| spl865_47 ),
inference(avatar_component_clause,[],[f28657]) ).
fof(f28663,definition,
( spl865_49
<=> v3_struct_0(k1_lattice2(sK36)) ),
introduced(definition,[new_symbols(definition,[spl865_49])],[avatar_definition]) ).
fof(f28664,plain,
( v3_struct_0(k1_lattice2(sK36))
| ~ spl865_49 ),
inference(avatar_component_clause,[],[f28663]) ).
fof(f28671,plain,
( m2_filter_2(k1_filter_0(sK36),k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) ),
inference(forward_demodulation,[],[f28649,f28557]) ).
fof(f28673,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| v3_struct_0(k1_lattice2(sK36))
| k2_filter_0(k1_lattice2(sK36),X0) = k2_filter_2(k1_lattice2(sK36),X0)
| ~ l3_lattices(k1_lattice2(sK36)) ),
inference(forward_demodulation,[],[f28647,f28557]) ).
fof(f28689,definition,
( spl865_53
<=> m2_filter_2(k1_filter_0(sK36),k1_lattice2(sK36)) ),
introduced(definition,[new_symbols(definition,[spl865_53])],[avatar_definition]) ).
fof(f28690,plain,
( m2_filter_2(k1_filter_0(sK36),k1_lattice2(sK36))
| ~ spl865_53 ),
inference(avatar_component_clause,[],[f28689]) ).
fof(f28691,plain,
( ~ spl865_47
| spl865_49
| spl865_53 ),
inference(avatar_split_clause,[],[f28671,f28689,f28663,f28657]) ).
fof(f28697,definition,
( spl865_55
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| k2_filter_0(k1_lattice2(sK36),X0) = k2_filter_2(k1_lattice2(sK36),X0) ) ),
introduced(definition,[new_symbols(definition,[spl865_55])],[avatar_definition]) ).
fof(f28698,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| k2_filter_0(k1_lattice2(sK36),X0) = k2_filter_2(k1_lattice2(sK36),X0) )
| ~ spl865_55 ),
inference(avatar_component_clause,[],[f28697]) ).
fof(f28699,plain,
( ~ spl865_47
| spl865_49
| spl865_55 ),
inference(avatar_split_clause,[],[f28673,f28697,f28663,f28657]) ).
fof(f28709,plain,
( ~ l3_lattices(sK36)
| spl865_47 ),
inference(resolution,[],[f28658,f19965]) ).
fof(f28711,plain,
( $false
| spl865_47 ),
inference(forward_subsumption_resolution,[],[f28709,f19815]) ).
fof(f28712,plain,
spl865_47,
inference(avatar_contradiction_clause,[],[f28711]) ).
fof(f28714,plain,
( v3_struct_0(sK36)
| ~ l3_lattices(sK36)
| ~ spl865_49 ),
inference(resolution,[],[f28664,f19978]) ).
fof(f28716,plain,
( ~ l3_lattices(sK36)
| ~ spl865_49 ),
inference(forward_subsumption_resolution,[],[f28714,f19817]) ).
fof(f28717,plain,
( $false
| ~ spl865_49 ),
inference(forward_subsumption_resolution,[],[f28716,f19815]) ).
fof(f28718,plain,
~ spl865_49,
inference(avatar_contradiction_clause,[],[f28717]) ).
fof(f28756,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| r3_lattices(sK36,X0,k6_lattices(sK36))
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f20295,f19821]) ).
fof(f28757,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| ~ v10_lattices(sK36)
| r3_lattices(sK36,X0,k6_lattices(sK36))
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28756,f19817]) ).
fof(f28758,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| r3_lattices(sK36,X0,k6_lattices(sK36))
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28757,f19816]) ).
fof(f28759,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| r3_lattices(sK36,X0,k6_lattices(sK36)) ),
inference(forward_subsumption_resolution,[],[f28758,f19815]) ).
fof(f28760,plain,
! [X0] :
( ~ m1_subset_1(X0,k17_filter_2(sK36))
| r3_lattices(sK36,X0,k6_lattices(sK36)) ),
inference(forward_demodulation,[],[f28759,f28534]) ).
fof(f28761,plain,
! [X0] :
( r3_lattices(sK36,X0,k6_lattices(sK36))
| ~ m1_subset_1(X0,k1_filter_0(sK36)) ),
inference(forward_demodulation,[],[f28760,f28540]) ).
fof(f28764,plain,
( k2_filter_0(k1_lattice2(sK36),sK37) = k2_filter_2(k1_lattice2(sK36),sK37)
| ~ spl865_55 ),
inference(resolution,[],[f28698,f28541]) ).
fof(f28880,definition,
( spl865_68
<=> r2_hidden(sK37,k18_filter_2(sK36,sK37)) ),
introduced(definition,[new_symbols(definition,[spl865_68])],[avatar_definition]) ).
fof(f28881,plain,
( ~ r2_hidden(sK37,k18_filter_2(sK36,sK37))
| spl865_68 ),
inference(avatar_component_clause,[],[f28880]) ).
fof(f28884,plain,
( $false
| spl865_68 ),
inference(unit_resulting_resolution,[],[f19801,f19815,f19816,f19817,f19818,f19818,f28881]) ).
fof(f28889,plain,
spl865_68,
inference(avatar_contradiction_clause,[],[f28884]) ).
fof(f28896,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| v3_struct_0(sK36)
| k5_filter_2(sK36,X0) = X0
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f19754,f19816]) ).
fof(f28899,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| k5_filter_2(sK36,X0) = X0
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28896,f19817]) ).
fof(f28904,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| k5_filter_2(sK36,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f28899,f19815]) ).
fof(f28905,plain,
! [X0] :
( ~ m1_subset_1(X0,k17_filter_2(sK36))
| k5_filter_2(sK36,X0) = X0 ),
inference(forward_demodulation,[],[f28904,f28534]) ).
fof(f28906,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| k5_filter_2(sK36,X0) = X0 ),
inference(forward_demodulation,[],[f28905,f28540]) ).
fof(f28907,plain,
sK37 = k5_filter_2(sK36,sK37),
inference(resolution,[],[f28906,f28541]) ).
fof(f28944,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| v3_struct_0(sK36)
| k18_filter_2(sK36,X0) = k2_filter_2(k1_lattice2(sK36),k5_filter_2(sK36,X0))
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f19798,f19816]) ).
fof(f28947,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| k18_filter_2(sK36,X0) = k2_filter_2(k1_lattice2(sK36),k5_filter_2(sK36,X0))
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f28944,f19817]) ).
fof(f28952,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK36))
| k18_filter_2(sK36,X0) = k2_filter_2(k1_lattice2(sK36),k5_filter_2(sK36,X0)) ),
inference(forward_subsumption_resolution,[],[f28947,f19815]) ).
fof(f28953,plain,
! [X0] :
( ~ m1_subset_1(X0,k17_filter_2(sK36))
| k18_filter_2(sK36,X0) = k2_filter_2(k1_lattice2(sK36),k5_filter_2(sK36,X0)) ),
inference(forward_demodulation,[],[f28952,f28534]) ).
fof(f28954,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| k18_filter_2(sK36,X0) = k2_filter_2(k1_lattice2(sK36),k5_filter_2(sK36,X0)) ),
inference(forward_demodulation,[],[f28953,f28540]) ).
fof(f28955,plain,
k18_filter_2(sK36,sK37) = k2_filter_2(k1_lattice2(sK36),k5_filter_2(sK36,sK37)),
inference(resolution,[],[f28954,f28541]) ).
fof(f28956,plain,
k2_filter_2(k1_lattice2(sK36),sK37) = k18_filter_2(sK36,sK37),
inference(forward_demodulation,[],[f28955,f28907]) ).
fof(f28958,plain,
( k2_filter_0(k1_lattice2(sK36),sK37) = k18_filter_2(sK36,sK37)
| ~ spl865_55 ),
inference(superposition,[],[f28764,f28956]) ).
fof(f28960,plain,
( m1_filter_0(k18_filter_2(sK36,sK37),k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ m1_subset_1(sK37,u1_struct_0(k1_lattice2(sK36)))
| ~ spl865_55 ),
inference(superposition,[],[f19882,f28958]) ).
fof(f28961,plain,
( ! [X0] :
( k2_filter_0(k1_lattice2(sK36),X0) != k18_filter_2(sK36,sK37)
| sK37 = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK36)))
| ~ m1_subset_1(sK37,u1_struct_0(k1_lattice2(sK36)))
| v3_struct_0(k1_lattice2(sK36))
| ~ v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) )
| ~ spl865_55 ),
inference(superposition,[],[f19881,f28958]) ).
fof(f28966,plain,
( ! [X0] :
( k2_filter_0(k1_lattice2(sK36),X0) != k18_filter_2(sK36,sK37)
| sK37 = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK36)))
| ~ m1_subset_1(sK37,u1_struct_0(k1_lattice2(sK36)))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) )
| ~ spl865_55 ),
inference(forward_subsumption_resolution,[],[f28961,f28646]) ).
fof(f28967,plain,
( m1_filter_0(k18_filter_2(sK36,sK37),k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ m1_subset_1(sK37,u1_struct_0(k1_lattice2(sK36)))
| ~ spl865_55 ),
inference(forward_subsumption_resolution,[],[f28960,f28646]) ).
fof(f28971,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| k2_filter_0(k1_lattice2(sK36),X0) != k18_filter_2(sK36,sK37)
| sK37 = X0
| ~ m1_subset_1(sK37,u1_struct_0(k1_lattice2(sK36)))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) )
| ~ spl865_55 ),
inference(forward_demodulation,[],[f28966,f28557]) ).
fof(f28972,plain,
( ~ m1_subset_1(sK37,k1_filter_0(sK36))
| m1_filter_0(k18_filter_2(sK36,sK37),k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ spl865_55 ),
inference(forward_demodulation,[],[f28967,f28557]) ).
fof(f28976,plain,
( ! [X0] :
( ~ m1_subset_1(sK37,k1_filter_0(sK36))
| ~ m1_subset_1(X0,k1_filter_0(sK36))
| k2_filter_0(k1_lattice2(sK36),X0) != k18_filter_2(sK36,sK37)
| sK37 = X0
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) )
| ~ spl865_55 ),
inference(forward_demodulation,[],[f28971,f28557]) ).
fof(f28977,plain,
( m1_filter_0(k18_filter_2(sK36,sK37),k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ spl865_55 ),
inference(forward_subsumption_resolution,[],[f28972,f28541]) ).
fof(f28981,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| k2_filter_0(k1_lattice2(sK36),X0) != k18_filter_2(sK36,sK37)
| sK37 = X0
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) )
| ~ spl865_55 ),
inference(forward_subsumption_resolution,[],[f28976,f28541]) ).
fof(f28983,definition,
( spl865_73
<=> m1_filter_0(k18_filter_2(sK36,sK37),k1_lattice2(sK36)) ),
introduced(definition,[new_symbols(definition,[spl865_73])],[avatar_definition]) ).
fof(f28984,plain,
( m1_filter_0(k18_filter_2(sK36,sK37),k1_lattice2(sK36))
| ~ spl865_73 ),
inference(avatar_component_clause,[],[f28983]) ).
fof(f28985,plain,
( ~ spl865_47
| spl865_49
| spl865_73
| ~ spl865_55 ),
inference(avatar_split_clause,[],[f28977,f28697,f28983,f28663,f28657]) ).
fof(f28992,definition,
( spl865_75
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| sK37 = X0
| k2_filter_0(k1_lattice2(sK36),X0) != k18_filter_2(sK36,sK37) ) ),
introduced(definition,[new_symbols(definition,[spl865_75])],[avatar_definition]) ).
fof(f28993,plain,
( ! [X0] :
( k2_filter_0(k1_lattice2(sK36),X0) != k18_filter_2(sK36,sK37)
| sK37 = X0
| ~ m1_subset_1(X0,k1_filter_0(sK36)) )
| ~ spl865_75 ),
inference(avatar_component_clause,[],[f28992]) ).
fof(f28995,plain,
( ~ spl865_47
| spl865_49
| spl865_75
| ~ spl865_55 ),
inference(avatar_split_clause,[],[f28981,f28697,f28992,f28663,f28657]) ).
fof(f28998,definition,
( spl865_76
<=> k1_filter_0(sK36) = k18_filter_2(sK36,sK37) ),
introduced(definition,[new_symbols(definition,[spl865_76])],[avatar_definition]) ).
fof(f28999,plain,
( k1_filter_0(sK36) != k18_filter_2(sK36,sK37)
| spl865_76 ),
inference(avatar_component_clause,[],[f28998]) ).
fof(f29004,plain,
( m1_filter_2(k18_filter_2(sK36,sK37),k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ spl865_73 ),
inference(resolution,[],[f28984,f19654]) ).
fof(f29005,plain,
( m1_filter_2(k18_filter_2(sK36,sK37),k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ spl865_73 ),
inference(forward_subsumption_resolution,[],[f29004,f28646]) ).
fof(f29007,definition,
( spl865_78
<=> m1_filter_2(k18_filter_2(sK36,sK37),k1_lattice2(sK36)) ),
introduced(definition,[new_symbols(definition,[spl865_78])],[avatar_definition]) ).
fof(f29008,plain,
( m1_filter_2(k18_filter_2(sK36,sK37),k1_lattice2(sK36))
| ~ spl865_78 ),
inference(avatar_component_clause,[],[f29007]) ).
fof(f29009,plain,
( ~ spl865_47
| spl865_49
| spl865_78
| ~ spl865_73 ),
inference(avatar_split_clause,[],[f29005,f28983,f29007,f28663,f28657]) ).
fof(f29033,plain,
( v13_lattices(k1_lattice2(sK36))
| v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f19933,f19821]) ).
fof(f29034,plain,
( v13_lattices(k1_lattice2(sK36))
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f29033,f19817]) ).
fof(f29035,plain,
( v13_lattices(k1_lattice2(sK36))
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f29034,f19816]) ).
fof(f29036,plain,
v13_lattices(k1_lattice2(sK36)),
inference(forward_subsumption_resolution,[],[f29035,f19815]) ).
fof(f29037,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK36))
| ~ v10_lattices(k1_lattice2(sK36))
| u1_struct_0(k1_lattice2(sK36)) = X0
| ~ l3_lattices(k1_lattice2(sK36))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK36)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK36)) ),
inference(resolution,[],[f29036,f27669]) ).
fof(f29040,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK36))
| u1_struct_0(k1_lattice2(sK36)) = X0
| ~ l3_lattices(k1_lattice2(sK36))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK36)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK36)) ),
inference(forward_subsumption_resolution,[],[f29037,f28646]) ).
fof(f29042,plain,
! [X0] :
( k1_filter_0(sK36) = X0
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK36)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK36)) ),
inference(forward_demodulation,[],[f29040,f28557]) ).
fof(f29047,plain,
! [X0] :
( ~ r2_hidden(k6_lattices(sK36),X0)
| k1_filter_0(sK36) = X0
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ m1_filter_0(X0,k1_lattice2(sK36)) ),
inference(forward_demodulation,[],[f29042,f28531]) ).
fof(f29049,definition,
( spl865_82
<=> ! [X0] :
( ~ r2_hidden(k6_lattices(sK36),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK36))
| k1_filter_0(sK36) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl865_82])],[avatar_definition]) ).
fof(f29050,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK36))
| ~ r2_hidden(k6_lattices(sK36),X0)
| k1_filter_0(sK36) = X0 )
| ~ spl865_82 ),
inference(avatar_component_clause,[],[f29049]) ).
fof(f29051,plain,
( ~ spl865_47
| spl865_49
| spl865_82 ),
inference(avatar_split_clause,[],[f29047,f29049,f28663,f28657]) ).
fof(f29054,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK36),k2_filter_0(k1_lattice2(sK36),X0))
| k1_filter_0(sK36) = k2_filter_0(k1_lattice2(sK36),X0)
| v3_struct_0(k1_lattice2(sK36))
| ~ v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK36))) )
| ~ spl865_82 ),
inference(resolution,[],[f29050,f19882]) ).
fof(f29057,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK36),k2_filter_0(k1_lattice2(sK36),X0))
| k1_filter_0(sK36) = k2_filter_0(k1_lattice2(sK36),X0)
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK36))) )
| ~ spl865_82 ),
inference(forward_subsumption_resolution,[],[f29054,f28646]) ).
fof(f29058,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| ~ r2_hidden(k6_lattices(sK36),k2_filter_0(k1_lattice2(sK36),X0))
| k1_filter_0(sK36) = k2_filter_0(k1_lattice2(sK36),X0)
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) )
| ~ spl865_82 ),
inference(forward_demodulation,[],[f29057,f28557]) ).
fof(f29060,definition,
( spl865_83
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| k1_filter_0(sK36) = k2_filter_0(k1_lattice2(sK36),X0)
| ~ r2_hidden(k6_lattices(sK36),k2_filter_0(k1_lattice2(sK36),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl865_83])],[avatar_definition]) ).
fof(f29061,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| k1_filter_0(sK36) = k2_filter_0(k1_lattice2(sK36),X0)
| ~ r2_hidden(k6_lattices(sK36),k2_filter_0(k1_lattice2(sK36),X0)) )
| ~ spl865_83 ),
inference(avatar_component_clause,[],[f29060]) ).
fof(f29062,plain,
( ~ spl865_47
| spl865_49
| spl865_83
| ~ spl865_82 ),
inference(avatar_split_clause,[],[f29058,f29049,f29060,f28663,f28657]) ).
fof(f29341,plain,
! [X0] :
( r2_hidden(k5_lattices(k1_lattice2(sK36)),X0)
| ~ m2_filter_2(X0,k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) ),
inference(resolution,[],[f19789,f29036]) ).
fof(f29342,plain,
! [X0] :
( r2_hidden(k5_lattices(k1_lattice2(sK36)),X0)
| ~ m2_filter_2(X0,k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) ),
inference(forward_subsumption_resolution,[],[f29341,f28646]) ).
fof(f29343,plain,
! [X0] :
( r2_hidden(k6_lattices(sK36),X0)
| ~ m2_filter_2(X0,k1_lattice2(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36)) ),
inference(forward_demodulation,[],[f29342,f28531]) ).
fof(f29345,definition,
( spl865_124
<=> ! [X0] :
( r2_hidden(k6_lattices(sK36),X0)
| ~ m2_filter_2(X0,k1_lattice2(sK36)) ) ),
introduced(definition,[new_symbols(definition,[spl865_124])],[avatar_definition]) ).
fof(f29346,plain,
( ! [X0] :
( r2_hidden(k6_lattices(sK36),X0)
| ~ m2_filter_2(X0,k1_lattice2(sK36)) )
| ~ spl865_124 ),
inference(avatar_component_clause,[],[f29345]) ).
fof(f29347,plain,
( ~ spl865_47
| spl865_49
| spl865_124 ),
inference(avatar_split_clause,[],[f29343,f29345,f28663,f28657]) ).
fof(f29438,plain,
( ! [X0] :
( ~ m2_filter_2(X0,k1_lattice2(sK36))
| m1_subset_1(k6_lattices(sK36),X0) )
| ~ spl865_124 ),
inference(resolution,[],[f20207,f29346]) ).
fof(f29445,plain,
( m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| ~ spl865_53
| ~ spl865_124 ),
inference(resolution,[],[f29438,f28690]) ).
fof(f29550,plain,
( m2_filter_2(k18_filter_2(sK36,sK37),sK36)
| v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36)
| ~ spl865_78 ),
inference(resolution,[],[f29008,f19767]) ).
fof(f29552,plain,
( m2_filter_2(k18_filter_2(sK36,sK37),sK36)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36)
| ~ spl865_78 ),
inference(forward_subsumption_resolution,[],[f29550,f19817]) ).
fof(f29553,plain,
( m2_filter_2(k18_filter_2(sK36,sK37),sK36)
| ~ l3_lattices(sK36)
| ~ spl865_78 ),
inference(forward_subsumption_resolution,[],[f29552,f19816]) ).
fof(f29554,plain,
( m2_filter_2(k18_filter_2(sK36,sK37),sK36)
| ~ spl865_78 ),
inference(forward_subsumption_resolution,[],[f29553,f19815]) ).
fof(f29560,plain,
( r2_filter_2(sK36,sK35(sK36,k18_filter_2(sK36,sK37)))
| u1_struct_0(sK36) = k18_filter_2(sK36,sK37)
| ~ v14_lattices(sK36)
| v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36)
| ~ spl865_78 ),
inference(resolution,[],[f29554,f19812]) ).
fof(f29561,plain,
( r2_filter_2(sK36,sK35(sK36,k18_filter_2(sK36,sK37)))
| u1_struct_0(sK36) = k18_filter_2(sK36,sK37)
| v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36)
| ~ spl865_78 ),
inference(forward_subsumption_resolution,[],[f29560,f19821]) ).
fof(f29563,plain,
( r2_filter_2(sK36,sK35(sK36,k18_filter_2(sK36,sK37)))
| u1_struct_0(sK36) = k18_filter_2(sK36,sK37)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36)
| ~ spl865_78 ),
inference(forward_subsumption_resolution,[],[f29561,f19817]) ).
fof(f29568,plain,
( r2_filter_2(sK36,sK35(sK36,k18_filter_2(sK36,sK37)))
| u1_struct_0(sK36) = k18_filter_2(sK36,sK37)
| ~ l3_lattices(sK36)
| ~ spl865_78 ),
inference(forward_subsumption_resolution,[],[f29563,f19816]) ).
fof(f29569,plain,
( r2_filter_2(sK36,sK35(sK36,k18_filter_2(sK36,sK37)))
| u1_struct_0(sK36) = k18_filter_2(sK36,sK37)
| ~ spl865_78 ),
inference(forward_subsumption_resolution,[],[f29568,f19815]) ).
fof(f29570,plain,
( k17_filter_2(sK36) = k18_filter_2(sK36,sK37)
| r2_filter_2(sK36,sK35(sK36,k18_filter_2(sK36,sK37)))
| ~ spl865_78 ),
inference(forward_demodulation,[],[f29569,f28534]) ).
fof(f29571,plain,
( k1_filter_0(sK36) = k18_filter_2(sK36,sK37)
| r2_filter_2(sK36,sK35(sK36,k18_filter_2(sK36,sK37)))
| ~ spl865_78 ),
inference(forward_demodulation,[],[f29570,f28540]) ).
fof(f29572,plain,
( r2_filter_2(sK36,sK35(sK36,k18_filter_2(sK36,sK37)))
| spl865_76
| ~ spl865_78 ),
inference(forward_subsumption_resolution,[],[f29571,f28999]) ).
fof(f29918,plain,
( r2_hidden(sK37,k18_filter_2(sK36,sK37))
| ~ spl865_68 ),
inference(avatar_component_clause,[],[f28880]) ).
fof(f30199,plain,
( k1_filter_0(sK36) = k2_filter_0(k1_lattice2(sK36),k6_lattices(sK36))
| ~ r2_hidden(k6_lattices(sK36),k2_filter_0(k1_lattice2(sK36),k6_lattices(sK36)))
| ~ spl865_53
| ~ spl865_83
| ~ spl865_124 ),
inference(resolution,[],[f29061,f29445]) ).
fof(f30203,definition,
( spl865_164
<=> r2_hidden(k6_lattices(sK36),k2_filter_0(k1_lattice2(sK36),k6_lattices(sK36))) ),
introduced(definition,[new_symbols(definition,[spl865_164])],[avatar_definition]) ).
fof(f30204,plain,
( ~ r2_hidden(k6_lattices(sK36),k2_filter_0(k1_lattice2(sK36),k6_lattices(sK36)))
| spl865_164 ),
inference(avatar_component_clause,[],[f30203]) ).
fof(f30206,definition,
( spl865_165
<=> k1_filter_0(sK36) = k2_filter_0(k1_lattice2(sK36),k6_lattices(sK36)) ),
introduced(definition,[new_symbols(definition,[spl865_165])],[avatar_definition]) ).
fof(f30207,plain,
( k1_filter_0(sK36) = k2_filter_0(k1_lattice2(sK36),k6_lattices(sK36))
| ~ spl865_165 ),
inference(avatar_component_clause,[],[f30206]) ).
fof(f30208,plain,
( ~ spl865_164
| spl865_165
| ~ spl865_53
| ~ spl865_83
| ~ spl865_124 ),
inference(avatar_split_clause,[],[f30199,f29345,f29060,f28689,f30206,f30203]) ).
fof(f30361,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK36))
| ~ m1_subset_1(X1,u1_struct_0(sK36))
| v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36) ),
inference(superposition,[],[f27058,f28557]) ).
fof(f30362,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK36))
| ~ m1_subset_1(X1,u1_struct_0(sK36))
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f30361,f19817]) ).
fof(f30363,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK36))
| ~ m1_subset_1(X1,u1_struct_0(sK36))
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f30362,f19816]) ).
fof(f30364,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK36))
| ~ m1_subset_1(X1,u1_struct_0(sK36)) ),
inference(forward_subsumption_resolution,[],[f30363,f19815]) ).
fof(f30365,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k17_filter_2(sK36))
| ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(sK36)) ),
inference(forward_demodulation,[],[f30364,f28534]) ).
fof(f30366,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(sK36)) ),
inference(forward_demodulation,[],[f30365,f28540]) ).
fof(f30367,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(sK36)) ),
inference(duplicate_literal_removal,[],[f30366]) ).
fof(f30368,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k17_filter_2(sK36))
| ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0) ),
inference(forward_demodulation,[],[f30367,f28534]) ).
fof(f30369,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ m1_subset_1(X0,k1_filter_0(sK36))
| r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0) ),
inference(forward_demodulation,[],[f30368,f28540]) ).
fof(f30370,plain,
! [X0,X1] :
( r3_lattices(k1_lattice2(sK36),X0,X1)
| ~ m1_subset_1(X0,k1_filter_0(sK36))
| ~ m1_subset_1(X1,k1_filter_0(sK36))
| ~ r3_lattices(sK36,X1,X0) ),
inference(duplicate_literal_removal,[],[f30369]) ).
fof(f31561,plain,
( ~ r2_hidden(sK37,sK35(sK36,k18_filter_2(sK36,sK37)))
| ~ m2_filter_2(sK35(sK36,k18_filter_2(sK36,sK37)),sK36)
| spl865_76
| ~ spl865_78 ),
inference(resolution,[],[f29572,f19819]) ).
fof(f31563,definition,
( spl865_302
<=> m2_filter_2(sK35(sK36,k18_filter_2(sK36,sK37)),sK36) ),
introduced(definition,[new_symbols(definition,[spl865_302])],[avatar_definition]) ).
fof(f31564,plain,
( ~ m2_filter_2(sK35(sK36,k18_filter_2(sK36,sK37)),sK36)
| spl865_302 ),
inference(avatar_component_clause,[],[f31563]) ).
fof(f31566,definition,
( spl865_303
<=> r2_hidden(sK37,sK35(sK36,k18_filter_2(sK36,sK37))) ),
introduced(definition,[new_symbols(definition,[spl865_303])],[avatar_definition]) ).
fof(f31567,plain,
( ~ r2_hidden(sK37,sK35(sK36,k18_filter_2(sK36,sK37)))
| spl865_303 ),
inference(avatar_component_clause,[],[f31566]) ).
fof(f31568,plain,
( ~ spl865_302
| ~ spl865_303
| spl865_76
| ~ spl865_78 ),
inference(avatar_split_clause,[],[f31561,f29007,f28998,f31566,f31563]) ).
fof(f31570,plain,
( k1_filter_0(sK36) = k18_filter_2(sK36,sK37)
| ~ m2_filter_2(k18_filter_2(sK36,sK37),sK36)
| spl865_302 ),
inference(resolution,[],[f31564,f28553]) ).
fof(f31575,plain,
( k1_filter_0(sK36) = k18_filter_2(sK36,sK37)
| ~ spl865_76 ),
inference(avatar_component_clause,[],[f28998]) ).
fof(f31588,plain,
( k1_filter_0(sK36) = k18_filter_2(sK36,sK37)
| ~ spl865_78
| spl865_302 ),
inference(forward_subsumption_resolution,[],[f31570,f29554]) ).
fof(f31595,plain,
( spl865_76
| ~ spl865_78
| spl865_302 ),
inference(avatar_split_clause,[],[f31588,f31563,f29007,f28998]) ).
fof(f32720,plain,
( k1_filter_0(sK36) != k18_filter_2(sK36,sK37)
| sK37 = k6_lattices(sK36)
| ~ m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| ~ spl865_75
| ~ spl865_165 ),
inference(superposition,[],[f28993,f30207]) ).
fof(f34699,plain,
( ~ r3_lattices(k1_lattice2(sK36),k6_lattices(sK36),k6_lattices(sK36))
| ~ m1_subset_1(k6_lattices(sK36),u1_struct_0(k1_lattice2(sK36)))
| ~ m1_subset_1(k6_lattices(sK36),u1_struct_0(k1_lattice2(sK36)))
| v3_struct_0(k1_lattice2(sK36))
| ~ v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| spl865_164 ),
inference(resolution,[],[f30204,f19888]) ).
fof(f34701,plain,
( ~ r3_lattices(k1_lattice2(sK36),k6_lattices(sK36),k6_lattices(sK36))
| ~ m1_subset_1(k6_lattices(sK36),u1_struct_0(k1_lattice2(sK36)))
| v3_struct_0(k1_lattice2(sK36))
| ~ v10_lattices(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| spl865_164 ),
inference(duplicate_literal_removal,[],[f34699]) ).
fof(f34709,plain,
( ~ r3_lattices(k1_lattice2(sK36),k6_lattices(sK36),k6_lattices(sK36))
| ~ m1_subset_1(k6_lattices(sK36),u1_struct_0(k1_lattice2(sK36)))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| spl865_164 ),
inference(forward_subsumption_resolution,[],[f34701,f28646]) ).
fof(f34711,plain,
( ~ m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| ~ r3_lattices(k1_lattice2(sK36),k6_lattices(sK36),k6_lattices(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| spl865_164 ),
inference(forward_demodulation,[],[f34709,f28557]) ).
fof(f34713,plain,
( ~ r3_lattices(k1_lattice2(sK36),k6_lattices(sK36),k6_lattices(sK36))
| v3_struct_0(k1_lattice2(sK36))
| ~ l3_lattices(k1_lattice2(sK36))
| ~ spl865_53
| ~ spl865_124
| spl865_164 ),
inference(forward_subsumption_resolution,[],[f34711,f29445]) ).
fof(f34716,definition,
( spl865_516
<=> r3_lattices(k1_lattice2(sK36),k6_lattices(sK36),k6_lattices(sK36)) ),
introduced(definition,[new_symbols(definition,[spl865_516])],[avatar_definition]) ).
fof(f34717,plain,
( ~ r3_lattices(k1_lattice2(sK36),k6_lattices(sK36),k6_lattices(sK36))
| spl865_516 ),
inference(avatar_component_clause,[],[f34716]) ).
fof(f34718,plain,
( ~ spl865_47
| spl865_49
| ~ spl865_516
| ~ spl865_53
| ~ spl865_124
| spl865_164 ),
inference(avatar_split_clause,[],[f34713,f30203,f29345,f28689,f34716,f28663,f28657]) ).
fof(f34720,plain,
( ~ m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| ~ m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| ~ r3_lattices(sK36,k6_lattices(sK36),k6_lattices(sK36))
| spl865_516 ),
inference(resolution,[],[f34717,f30370]) ).
fof(f34721,plain,
( ~ m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| ~ r3_lattices(sK36,k6_lattices(sK36),k6_lattices(sK36))
| spl865_516 ),
inference(duplicate_literal_removal,[],[f34720]) ).
fof(f34722,plain,
( ~ m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| spl865_516 ),
inference(forward_subsumption_resolution,[],[f34721,f28761]) ).
fof(f34723,plain,
( $false
| ~ spl865_53
| ~ spl865_124
| spl865_516 ),
inference(forward_subsumption_resolution,[],[f34722,f29445]) ).
fof(f34724,plain,
( ~ spl865_53
| ~ spl865_124
| spl865_516 ),
inference(avatar_contradiction_clause,[],[f34723]) ).
fof(f34725,plain,
( sK37 = k6_lattices(sK36)
| ~ m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| ~ spl865_75
| ~ spl865_76
| ~ spl865_165 ),
inference(forward_subsumption_resolution,[],[f32720,f31575]) ).
fof(f34726,plain,
( ~ m1_subset_1(k6_lattices(sK36),k1_filter_0(sK36))
| ~ spl865_75
| ~ spl865_76
| ~ spl865_165 ),
inference(forward_subsumption_resolution,[],[f34725,f19820]) ).
fof(f34727,plain,
( $false
| ~ spl865_53
| ~ spl865_75
| ~ spl865_76
| ~ spl865_124
| ~ spl865_165 ),
inference(forward_subsumption_resolution,[],[f34726,f29445]) ).
fof(f34728,plain,
( ~ spl865_53
| ~ spl865_75
| ~ spl865_76
| ~ spl865_124
| ~ spl865_165 ),
inference(avatar_contradiction_clause,[],[f34727]) ).
fof(f35246,plain,
! [X2,X0,X1] :
( ~ v14_lattices(X2)
| r2_hidden(X0,sK35(X2,X1))
| u1_struct_0(X2) = X1
| ~ m2_filter_2(X1,X2)
| ~ r2_hidden(X0,X1)
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) ),
inference(resolution,[],[f20496,f19813]) ).
fof(f35250,plain,
! [X0,X1] :
( r2_hidden(X0,sK35(sK36,X1))
| u1_struct_0(sK36) = X1
| ~ m2_filter_2(X1,sK36)
| ~ r2_hidden(X0,X1)
| v3_struct_0(sK36)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36) ),
inference(resolution,[],[f35246,f19821]) ).
fof(f35253,plain,
! [X0,X1] :
( r2_hidden(X0,sK35(sK36,X1))
| u1_struct_0(sK36) = X1
| ~ m2_filter_2(X1,sK36)
| ~ r2_hidden(X0,X1)
| ~ v10_lattices(sK36)
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f35250,f19817]) ).
fof(f35255,plain,
! [X0,X1] :
( r2_hidden(X0,sK35(sK36,X1))
| u1_struct_0(sK36) = X1
| ~ m2_filter_2(X1,sK36)
| ~ r2_hidden(X0,X1)
| ~ l3_lattices(sK36) ),
inference(forward_subsumption_resolution,[],[f35253,f19816]) ).
fof(f35260,plain,
! [X0,X1] :
( r2_hidden(X0,sK35(sK36,X1))
| u1_struct_0(sK36) = X1
| ~ m2_filter_2(X1,sK36)
| ~ r2_hidden(X0,X1) ),
inference(forward_subsumption_resolution,[],[f35255,f19815]) ).
fof(f35261,plain,
! [X0,X1] :
( k17_filter_2(sK36) = X1
| r2_hidden(X0,sK35(sK36,X1))
| ~ m2_filter_2(X1,sK36)
| ~ r2_hidden(X0,X1) ),
inference(forward_demodulation,[],[f35260,f28534]) ).
fof(f35262,plain,
! [X0,X1] :
( r2_hidden(X0,sK35(sK36,X1))
| k1_filter_0(sK36) = X1
| ~ m2_filter_2(X1,sK36)
| ~ r2_hidden(X0,X1) ),
inference(forward_demodulation,[],[f35261,f28540]) ).
fof(f35267,plain,
( k1_filter_0(sK36) = k18_filter_2(sK36,sK37)
| ~ m2_filter_2(k18_filter_2(sK36,sK37),sK36)
| ~ r2_hidden(sK37,k18_filter_2(sK36,sK37))
| spl865_303 ),
inference(resolution,[],[f35262,f31567]) ).
fof(f35278,plain,
( ~ m2_filter_2(k18_filter_2(sK36,sK37),sK36)
| ~ r2_hidden(sK37,k18_filter_2(sK36,sK37))
| spl865_76
| spl865_303 ),
inference(forward_subsumption_resolution,[],[f35267,f28999]) ).
fof(f35281,plain,
( ~ r2_hidden(sK37,k18_filter_2(sK36,sK37))
| spl865_76
| ~ spl865_78
| spl865_303 ),
inference(forward_subsumption_resolution,[],[f35278,f29554]) ).
fof(f35282,plain,
( $false
| ~ spl865_68
| spl865_76
| ~ spl865_78
| spl865_303 ),
inference(forward_subsumption_resolution,[],[f35281,f29918]) ).
fof(f35283,plain,
( ~ spl865_68
| spl865_76
| ~ spl865_78
| spl865_303 ),
inference(avatar_contradiction_clause,[],[f35282]) ).
cnf(s43,plain,
( ~ spl865_47
| spl865_49
| spl865_53 ),
inference(sat_conversion,[],[f28691]) ).
cnf(s45,plain,
( ~ spl865_47
| spl865_49
| spl865_55 ),
inference(sat_conversion,[],[f28699]) ).
cnf(s49,plain,
spl865_47,
inference(sat_conversion,[],[f28712]) ).
cnf(s51,plain,
~ spl865_49,
inference(sat_conversion,[],[f28718]) ).
cnf(s63,plain,
spl865_68,
inference(sat_conversion,[],[f28889]) ).
cnf(s69,plain,
( ~ spl865_47
| spl865_49
| ~ spl865_55
| spl865_73 ),
inference(sat_conversion,[],[f28985]) ).
cnf(s72,plain,
( ~ spl865_47
| spl865_49
| ~ spl865_55
| spl865_75 ),
inference(sat_conversion,[],[f28995]) ).
cnf(s74,plain,
( ~ spl865_47
| spl865_49
| ~ spl865_73
| spl865_78 ),
inference(sat_conversion,[],[f29009]) ).
cnf(s78,plain,
( ~ spl865_47
| spl865_49
| spl865_82 ),
inference(sat_conversion,[],[f29051]) ).
cnf(s79,plain,
( ~ spl865_47
| spl865_49
| ~ spl865_82
| spl865_83 ),
inference(sat_conversion,[],[f29062]) ).
cnf(s115,plain,
( ~ spl865_47
| spl865_49
| spl865_124 ),
inference(sat_conversion,[],[f29347]) ).
cnf(s156,plain,
( ~ spl865_53
| ~ spl865_83
| ~ spl865_124
| ~ spl865_164
| spl865_165 ),
inference(sat_conversion,[],[f30208]) ).
cnf(s275,plain,
( spl865_76
| ~ spl865_78
| ~ spl865_302
| ~ spl865_303 ),
inference(sat_conversion,[],[f31568]) ).
cnf(s284,plain,
( spl865_76
| ~ spl865_78
| spl865_302 ),
inference(sat_conversion,[],[f31595]) ).
cnf(s506,plain,
( ~ spl865_47
| spl865_49
| ~ spl865_53
| ~ spl865_124
| spl865_164
| ~ spl865_516 ),
inference(sat_conversion,[],[f34718]) ).
cnf(s507,plain,
( ~ spl865_53
| ~ spl865_124
| spl865_516 ),
inference(sat_conversion,[],[f34724]) ).
cnf(s508,plain,
( ~ spl865_53
| ~ spl865_75
| ~ spl865_76
| ~ spl865_124
| ~ spl865_165 ),
inference(sat_conversion,[],[f34728]) ).
cnf(s571,plain,
( ~ spl865_68
| spl865_76
| ~ spl865_78
| spl865_303 ),
inference(sat_conversion,[],[f35283]) ).
cnf(s675,plain,
spl865_124,
inference(rat,[],[s115,s51,s49]) ).
cnf(s682,plain,
spl865_82,
inference(rat,[],[s78,s51,s49]) ).
cnf(s705,plain,
spl865_83,
inference(rat,[],[s79,s49,s51,s682]) ).
cnf(s715,plain,
spl865_55,
inference(rat,[],[s45,s51,s49]) ).
cnf(s722,plain,
spl865_75,
inference(rat,[],[s72,s49,s51,s715]) ).
cnf(s724,plain,
spl865_73,
inference(rat,[],[s69,s49,s51,s715]) ).
cnf(s725,plain,
spl865_78,
inference(rat,[],[s74,s49,s51,s724]) ).
cnf(s731,plain,
spl865_53,
inference(rat,[],[s43,s51,s49]) ).
cnf(s732,plain,
spl865_516,
inference(rat,[],[s507,s675,s731]) ).
cnf(s739,plain,
spl865_164,
inference(rat,[],[s506,s732,s675,s49,s51,s731]) ).
cnf(s745,plain,
spl865_165,
inference(rat,[],[s156,s731,s705,s675,s739]) ).
cnf(s748,plain,
~ spl865_76,
inference(rat,[],[s508,s731,s675,s722,s745]) ).
cnf(s749,plain,
spl865_303,
inference(rat,[],[s571,s725,s63,s748]) ).
cnf(s754,plain,
spl865_302,
inference(rat,[],[s284,s725,s748]) ).
cnf(s757,plain,
$false,
inference(rat,[],[s275,s749,s725,s754,s748]) ).
fof(f35284,plain,
$false,
inference(avatar_sat_refutation,[],[s757]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT309+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 14:26:11 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.40 Running first-order theorem proving
% 0.10/0.40 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
% 20.66/4.94 % (1468690)Detected formulas, will run a generic FOF schedule.
% 20.66/4.94 % (1468814)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4144330945:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 20.66/4.94 % (1468814)Instruction limit reached!
% 20.66/4.94 % (1468814)------------------------------
% 20.66/4.94 % (1468814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/4.94 % (1468814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/4.94 % (1468814)CaDiCaL version: 2.1.3
% 20.66/4.94 % (1468814)Termination reason: Instruction limit
% 20.66/4.94 % (1468814)Termination phase: Property scanning
% 20.66/4.94 % (1468814)Time elapsed: 0.056 s
% 20.66/4.94 % (1468814)Peak memory usage: 102 MB
% 20.66/4.94 % (1468814)Instructions burned: 141 (million)
% 20.66/4.94 % (1468810)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=240965572:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 20.66/4.94 % (1468811)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=986697931:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 20.66/4.94 % (1468813)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4045506518:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 20.66/4.94 % (1468809)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=939623892:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 20.66/4.94 % (1468812)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1130632489:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 20.66/4.94 % (1468815)dis-21_1_sil=8000:lcm=predicate:random_seed=3612009865:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 20.66/4.94 % (1468812)Refutation not found, incomplete strategy
% 20.66/4.94 % (1468812)------------------------------
% 20.66/4.94 % (1468812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/4.94 % (1468812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/4.94 % (1468812)CaDiCaL version: 2.1.3
% 20.66/4.94 % (1468812)Termination reason: Refutation not found, incomplete strategy
% 20.66/4.94 % (1468812)Time elapsed: 0.103 s
% 20.66/4.94 % (1468812)Peak memory usage: 107 MB
% 20.66/4.94 % (1468812)Instructions burned: 83 (million)
% 20.66/4.94 % (1468813)Instruction limit reached!
% 20.66/4.94 % (1468813)------------------------------
% 20.66/4.94 % (1468813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/4.94 % (1468813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/4.94 % (1468813)CaDiCaL version: 2.1.3
% 20.66/4.94 % (1468813)Termination reason: Instruction limit
% 20.66/4.94 % (1468813)Termination phase: Function definition elimination
% 20.66/4.94 % (1468813)Time elapsed: 0.140 s
% 20.66/4.94 % (1468813)Peak memory usage: 105 MB
% 20.66/4.94 % (1468813)Instructions burned: 120 (million)
% 20.66/4.94 % (1468815)Instruction limit reached!
% 20.66/4.94 % (1468815)------------------------------
% 20.66/4.94 % (1468815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/4.94 % (1468815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/4.94 % (1468815)CaDiCaL version: 2.1.3
% 20.66/4.94 % (1468815)Termination reason: Instruction limit
% 20.66/4.94 % (1468815)Termination phase: Preprocessing 1
% 20.66/4.94 % (1468815)Time elapsed: 0.146 s
% 20.66/4.94 % (1468815)Peak memory usage: 104 MB
% 20.66/4.94 % (1468815)Instructions burned: 130 (million)
% 20.66/4.94 % (1468835)lrs+10_1_sil=8000:sp=occurrence:random_seed=896102544:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 20.66/4.94 % (1468841)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1984418461:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/157Mi)
% 20.66/4.94 % (1468835)Instruction limit reached!
% 20.66/4.94 % (1468835)------------------------------
% 20.66/4.94 % (1468835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/4.94 % (1468835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/4.94 % (1468835)CaDiCaL version: 2.1.3
% 20.66/4.94 % (1468835)Termination reason: Instruction limit
% 35.54/6.57 % (1468835)Termination phase: Saturation
% 35.54/6.57 % (1468835)Time elapsed: 0.171 s
% 35.54/6.57 % (1468835)Peak memory usage: 110 MB
% 35.54/6.57 % (1468835)Instructions burned: 286 (million)
% 35.54/6.57 % (1468844)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1722396273:i=325:sd=1:ss=axioms:sgt=32_2989 on theBenchmark for (2989ds/325Mi)
% 35.54/6.57 % (1468841)Instruction limit reached!
% 35.54/6.57 % (1468841)------------------------------
% 35.54/6.57 % (1468841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.57 % (1468841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.57 % (1468841)CaDiCaL version: 2.1.3
% 35.54/6.57 % (1468841)Termination reason: Instruction limit
% 35.54/6.57 % (1468841)Termination phase: Property scanning
% 35.54/6.57 % (1468841)Time elapsed: 0.128 s
% 35.54/6.57 % (1468841)Peak memory usage: 102 MB
% 35.54/6.57 % (1468841)Instructions burned: 157 (million)
% 35.54/6.57 % (1468812)------------------------------
% 35.54/6.57 % (1468812)------------------------------
% 35.54/6.57 % (1468853)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=75441622:s2a=on:i=248:s2at=1.23:gtg=position_2987 on theBenchmark for (2987ds/248Mi)
% 35.54/6.57 % (1468853)Instruction limit reached!
% 35.54/6.57 % (1468853)------------------------------
% 35.54/6.57 % (1468853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.57 % (1468853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.57 % (1468853)CaDiCaL version: 2.1.3
% 35.54/6.57 % (1468853)Termination reason: Instruction limit
% 35.54/6.57 % (1468853)Termination phase: SInE selection
% 35.54/6.57 % (1468853)Time elapsed: 0.124 s
% 35.54/6.57 % (1468853)Peak memory usage: 103 MB
% 35.54/6.57 % (1468853)Instructions burned: 248 (million)
% 35.54/6.57 % (1468856)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4056970313:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 35.54/6.57 % (1468857)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=30166946:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 35.54/6.57 % (1468844)Instruction limit reached!
% 35.54/6.57 % (1468844)------------------------------
% 35.54/6.57 % (1468844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.57 % (1468844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.57 % (1468844)CaDiCaL version: 2.1.3
% 35.54/6.57 % (1468844)Termination reason: Instruction limit
% 35.54/6.57 % (1468844)Termination phase: Saturation
% 35.54/6.57 % (1468844)Time elapsed: 0.353 s
% 35.54/6.57 % (1468844)Peak memory usage: 108 MB
% 35.54/6.57 % (1468844)Instructions burned: 325 (million)
% 35.54/6.57 % (1468859)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=730723958:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 35.54/6.57 % (1468859)Instruction limit reached!
% 35.54/6.57 % (1468859)------------------------------
% 35.54/6.57 % (1468859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.57 % (1468859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.57 % (1468859)CaDiCaL version: 2.1.3
% 35.54/6.57 % (1468859)Termination reason: Instruction limit
% 35.54/6.57 % (1468859)Termination phase: Preprocessing 3
% 35.54/6.57 % (1468859)Time elapsed: 0.083 s
% 35.54/6.57 % (1468859)Peak memory usage: 105 MB
% 35.54/6.57 % (1468859)Instructions burned: 115 (million)
% 35.54/6.57 % (1468856)Instruction limit reached!
% 35.54/6.57 % (1468856)------------------------------
% 35.54/6.57 % (1468856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.57 % (1468856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.57 % (1468856)CaDiCaL version: 2.1.3
% 35.54/6.57 % (1468856)Termination reason: Instruction limit
% 35.54/6.57 % (1468856)Termination phase: Saturation
% 35.54/6.57 % (1468856)Time elapsed: 0.301 s
% 35.54/6.57 % (1468856)Peak memory usage: 110 MB
% 35.54/6.57 % (1468856)Instructions burned: 295 (million)
% 35.54/6.57 % (1468862)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2634700428:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 35.54/6.57 % (1468862)Instruction limit reached!
% 35.54/6.57 % (1468862)------------------------------
% 35.54/6.57 % (1468862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.57 % (1468862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468862)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468862)Termination reason: Instruction limit
% 25.46/7.58 % (1468862)Termination phase: Preprocessing 2
% 25.46/7.58 % (1468862)Time elapsed: 0.154 s
% 25.46/7.58 % (1468862)Peak memory usage: 106 MB
% 25.46/7.58 % (1468862)Instructions burned: 127 (million)
% 25.46/7.58 % (1468870)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3702370102:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 25.46/7.58 % (1468870)Instruction limit reached!
% 25.46/7.58 % (1468870)------------------------------
% 25.46/7.58 % (1468870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468870)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468870)Termination reason: Instruction limit
% 25.46/7.58 % (1468870)Termination phase: Property scanning
% 25.46/7.58 % (1468870)Time elapsed: 0.051 s
% 25.46/7.58 % (1468870)Peak memory usage: 102 MB
% 25.46/7.58 % (1468870)Instructions burned: 116 (million)
% 25.46/7.58 % (1468872)lrs+10_1_sil=8000:sp=occurrence:random_seed=1772492813:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 25.46/7.58 % (1468875)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4072881140:i=437:sd=1:aac=none:ss=included_2978 on theBenchmark for (2978ds/437Mi)
% 25.46/7.58 % (1468877)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=377267747:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 25.46/7.58 % (1468875)Instruction limit reached!
% 25.46/7.58 % (1468875)------------------------------
% 25.46/7.58 % (1468875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468875)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468875)Termination reason: Instruction limit
% 25.46/7.58 % (1468875)Termination phase: Saturation
% 25.46/7.58 % (1468875)Time elapsed: 0.425 s
% 25.46/7.58 % (1468875)Peak memory usage: 109 MB
% 25.46/7.58 % (1468875)Instructions burned: 438 (million)
% 25.46/7.58 % (1468887)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3472092550:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2971 on theBenchmark for (2971ds/134Mi)
% 25.46/7.58 % (1468872)Instruction limit reached!
% 25.46/7.58 % (1468872)------------------------------
% 25.46/7.58 % (1468872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468872)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468872)Termination reason: Instruction limit
% 25.46/7.58 % (1468872)Termination phase: Saturation
% 25.46/7.58 % (1468872)Time elapsed: 0.942 s
% 25.46/7.58 % (1468872)Peak memory usage: 121 MB
% 25.46/7.58 % (1468872)Instructions burned: 907 (million)
% 25.46/7.58 % (1468887)Instruction limit reached!
% 25.46/7.58 % (1468887)------------------------------
% 25.46/7.58 % (1468887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468887)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468887)Termination reason: Instruction limit
% 25.46/7.58 % (1468887)Termination phase: Property scanning
% 25.46/7.58 % (1468887)Time elapsed: 0.160 s
% 25.46/7.58 % (1468887)Peak memory usage: 106 MB
% 25.46/7.58 % (1468887)Instructions burned: 135 (million)
% 25.46/7.58 % (1468891)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1759397276:st=8:i=592:sd=3:ep=RST:ss=axioms_2968 on theBenchmark for (2968ds/592Mi)
% 25.46/7.58 % (1468892)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3013501003:st=3:i=13193:sd=3:ss=axioms_2967 on theBenchmark for (2967ds/13193Mi)
% 25.46/7.58 % (1468857)Instruction limit reached!
% 25.46/7.58 % (1468857)------------------------------
% 25.46/7.58 % (1468857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468857)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468857)Termination reason: Instruction limit
% 25.46/7.58 % (1468857)Termination phase: Saturation
% 25.46/7.58 % (1468857)Time elapsed: 2.365 s
% 25.46/7.58 % (1468857)Peak memory usage: 239 MB
% 25.46/7.58 % (1468857)Instructions burned: 2350 (million)
% 25.46/7.58 % (1468891)Instruction limit reached!
% 25.46/7.58 % (1468891)------------------------------
% 25.46/7.58 % (1468891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468891)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468891)Termination reason: Instruction limit
% 25.46/7.58 % (1468891)Termination phase: Property scanning
% 25.46/7.58 % (1468891)Time elapsed: 0.632 s
% 25.46/7.58 % (1468891)Peak memory usage: 124 MB
% 25.46/7.58 % (1468891)Instructions burned: 593 (million)
% 25.46/7.58 % (1468897)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=2946352015:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/125Mi)
% 25.46/7.58 % (1468898)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3348666252:i=134:gtgl=5:slsql=off:gtg=exists_sym_2959 on theBenchmark for (2959ds/134Mi)
% 25.46/7.58 % (1468897)Instruction limit reached!
% 25.46/7.58 % (1468897)------------------------------
% 25.46/7.58 % (1468897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468897)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468897)Termination reason: Instruction limit
% 25.46/7.58 % (1468897)Termination phase: Property scanning
% 25.46/7.58 % (1468897)Time elapsed: 0.106 s
% 25.46/7.58 % (1468897)Peak memory usage: 102 MB
% 25.46/7.58 % (1468897)Instructions burned: 125 (million)
% 25.46/7.58 % (1468898)Instruction limit reached!
% 25.46/7.58 % (1468898)------------------------------
% 25.46/7.58 % (1468898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468898)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468898)Termination reason: Instruction limit
% 25.46/7.58 % (1468898)Termination phase: Property scanning
% 25.46/7.58 % (1468898)Time elapsed: 0.114 s
% 25.46/7.58 % (1468898)Peak memory usage: 102 MB
% 25.46/7.58 % (1468898)Instructions burned: 134 (million)
% 25.46/7.58 % (1468901)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=955737830:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/141Mi)
% 25.46/7.58 % (1468902)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3266291029:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2954 on theBenchmark for (2954ds/431Mi)
% 25.46/7.58 % (1468901)Refutation not found, incomplete strategy
% 25.46/7.58 % (1468901)------------------------------
% 25.46/7.58 % (1468901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468901)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468901)Termination reason: Refutation not found, incomplete strategy
% 25.46/7.58 % (1468901)Time elapsed: 0.107 s
% 25.46/7.58 % (1468901)Peak memory usage: 107 MB
% 25.46/7.58 % (1468901)Instructions burned: 82 (million)
% 25.46/7.58 % (1468901)------------------------------
% 25.46/7.58 % (1468901)------------------------------
% 25.46/7.58 % (1468902)Instruction limit reached!
% 25.46/7.58 % (1468902)------------------------------
% 25.46/7.58 % (1468902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468902)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468902)Termination reason: Instruction limit
% 25.46/7.58 % (1468902)Termination phase: Saturation
% 25.46/7.58 % (1468902)Time elapsed: 0.439 s
% 25.46/7.58 % (1468902)Peak memory usage: 111 MB
% 25.46/7.58 % (1468902)Instructions burned: 432 (million)
% 25.46/7.58 % (1468908)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=2501717440:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2947 on theBenchmark for (2947ds/150Mi)
% 25.46/7.58 % (1468907)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=2695106256:i=6060:aac=none:ins=25_2947 on theBenchmark for (2947ds/6060Mi)
% 25.46/7.58 % (1468908)Instruction limit reached!
% 25.46/7.58 % (1468908)------------------------------
% 25.46/7.58 % (1468908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468908)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468908)Termination reason: Instruction limit
% 25.46/7.58 % (1468908)Termination phase: Preprocessing 1
% 25.46/7.58 % (1468908)Time elapsed: 0.172 s
% 25.46/7.58 % (1468908)Peak memory usage: 103 MB
% 25.46/7.58 % (1468908)Instructions burned: 150 (million)
% 25.46/7.58 % (1468877)Instruction limit reached!
% 25.46/7.58 % (1468877)------------------------------
% 25.46/7.58 % (1468877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468877)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468877)Termination reason: Instruction limit
% 25.46/7.58 % (1468877)Termination phase: Saturation
% 25.46/7.58 % (1468877)Time elapsed: 3.342 s
% 25.46/7.58 % (1468877)Peak memory usage: 404 MB
% 25.46/7.58 % (1468877)Instructions burned: 5204 (million)
% 25.46/7.58 % (1468911)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2088628080:i=14155:bd=all_2942 on theBenchmark for (2942ds/14155Mi)
% 25.46/7.58 % (1468912)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2092849685:i=667:av=off:fsr=off_2942 on theBenchmark for (2942ds/667Mi)
% 25.46/7.58 % (1468810)First to succeed.
% 25.46/7.58 % (1468810)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1468690"
% 25.46/7.58 % (1468912)Instruction limit reached!
% 25.46/7.58 % (1468912)------------------------------
% 25.46/7.58 % (1468912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.46/7.58 % (1468912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/7.58 % (1468912)CaDiCaL version: 2.1.3
% 25.46/7.58 % (1468912)Termination reason: Instruction limit
% 25.46/7.58 % (1468912)Termination phase: NewCNF
% 25.46/7.58 % (1468912)Time elapsed: 0.416 s
% 25.46/7.58 % (1468912)Peak memory usage: 135 MB
% 25.46/7.58 % (1468912)Instructions burned: 669 (million)
% 25.46/7.58 % (1468810)Refutation found. Thanks to Tanya!
% 25.46/7.58 % SZS status Theorem for theBenchmark
% 25.46/7.58 % SZS output start Proof for theBenchmark
% See solution above
% 43.76/7.82 % (1468810)------------------------------
% 43.76/7.82 % (1468810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.76/7.82 % (1468810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.76/7.82 % (1468810)CaDiCaL version: 2.1.3
% 43.76/7.82 % (1468810)Termination reason: Refutation
% 43.76/7.82 % (1468810)Time elapsed: 5.328 s
% 43.76/7.82 % (1468810)Peak memory usage: 246 MB
% 43.76/7.82 % (1468810)Instructions burned: 4997 (million)
% 43.76/7.82 % (1468810)------------------------------
% 43.76/7.82 % (1468810)------------------------------
% 43.76/7.82 % (1468690)Success in time 6.725 s
% 43.76/7.82 % Vampire exiting
%------------------------------------------------------------------------------