%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT309+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:46 AM UTC 2026
% Result : Theorem 13.69s 2.94s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 37
% Syntax : Number of formulae : 312 ( 48 unt; 15 def)
% Number of atoms : 1167 ( 159 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1421 ( 566 ~; 658 |; 134 &)
% ( 26 <=>; 37 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 38 ( 36 usr; 16 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 2 con; 0-3 aty)
% Number of variables : 250 ( 0 sgn 242 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f2410,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f2426,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> m1_subset_1(k6_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_lattices) ).
fof(f2456,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_0(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f2475,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/sandbox2/benchmark/theBenchmark.p',t32_filter_0) ).
fof(f2517,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_lattices(k8_filter_0(X0,k2_filter_0(X0,X1))) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t71_filter_0) ).
fof(f2543,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/sandbox2/benchmark/theBenchmark.p',dt_k2_filter_0) ).
fof(f2564,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f2569,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/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f2597,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/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f2645,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_lattice2) ).
fof(f2660,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/sandbox2/benchmark/theBenchmark.p',t79_lattice2) ).
fof(f2669,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f2872,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/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f2881,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/sandbox2/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f2936,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/sandbox2/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f2941,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/sandbox2/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f2953,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k17_filter_2(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f2956,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/sandbox2/benchmark/theBenchmark.p',t30_filter_2) ).
fof(f2957,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/sandbox2/benchmark/theBenchmark.p',t31_filter_2) ).
fof(f2961,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/sandbox2/benchmark/theBenchmark.p',t34_filter_2) ).
fof(f2963,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/sandbox2/benchmark/theBenchmark.p',t36_filter_2) ).
fof(f2964,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)],[f2963]) ).
fof(f2988,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,[],[f2872]) ).
fof(f2989,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,[],[f2988]) ).
fof(f3006,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,[],[f2881]) ).
fof(f3007,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,[],[f3006]) ).
fof(f3113,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,[],[f2936]) ).
fof(f3114,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,[],[f3113]) ).
fof(f3123,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,[],[f2941]) ).
fof(f3124,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,[],[f3123]) ).
fof(f3147,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2953]) ).
fof(f3148,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3147]) ).
fof(f3153,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,[],[f2956]) ).
fof(f3154,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,[],[f3153]) ).
fof(f3155,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,[],[f2957]) ).
fof(f3156,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,[],[f3155]) ).
fof(f3163,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,[],[f2961]) ).
fof(f3164,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,[],[f3163]) ).
fof(f3167,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,[],[f2964]) ).
fof(f3168,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,[],[f3167]) ).
fof(f3219,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,[],[f2475]) ).
fof(f3220,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,[],[f3219]) ).
fof(f3225,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2456]) ).
fof(f3226,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3225]) ).
fof(f3227,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,[],[f2543]) ).
fof(f3228,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,[],[f3227]) ).
fof(f3235,plain,
! [X0] :
( ! [X1] :
( k5_lattices(k8_filter_0(X0,k2_filter_0(X0,X1))) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2517]) ).
fof(f3236,plain,
! [X0] :
( ! [X1] :
( k5_lattices(k8_filter_0(X0,k2_filter_0(X0,X1))) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3235]) ).
fof(f3295,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f3298,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,[],[f2569]) ).
fof(f3299,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,[],[f3298]) ).
fof(f3300,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2564]) ).
fof(f3301,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3300]) ).
fof(f3467,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,[],[f2597]) ).
fof(f3468,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,[],[f3467]) ).
fof(f3531,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2645]) ).
fof(f3532,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3531]) ).
fof(f3535,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,[],[f2660]) ).
fof(f3536,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,[],[f3535]) ).
fof(f3650,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f3739,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2410]) ).
fof(f3741,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f2426]) ).
fof(f3742,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f3741]) ).
fof(f4810,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,[],[f2989]) ).
fof(f4830,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,[],[f3124]) ).
fof(f4845,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ( r1_tarski(X1,sK19(X0,X1))
& r2_filter_2(X0,sK19(X0,X1))
& m2_filter_2(sK19(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,[sK19]),skolemize(X2,sK19(X0,X1))],[f3164]) ).
fof(f4846,plain,
( v14_lattices(sK20)
& sK21 != k6_lattices(sK20)
& ! [X2] :
( ~ r2_hidden(sK21,X2)
| ~ r2_filter_2(sK20,X2)
| ~ m2_filter_2(X2,sK20) )
& m1_subset_1(sK21,u1_struct_0(sK20))
& ~ v3_struct_0(sK20)
& v10_lattices(sK20)
& l3_lattices(sK20) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21]),skolemize(X0,sK20),skolemize(X1,sK21)],[f3168]) ).
fof(f5025,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,[],[f3532]) ).
fof(f5059,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,[],[f3650]) ).
fof(f5060,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,[],[f5059]) ).
fof(f5061,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK152(X0,X1),X1)
& r2_hidden(sK152(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK152]),skolemize(X2,sK152(X0,X1))],[f5060]) ).
fof(f5477,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| m1_filter_2(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f4810]) ).
fof(f5488,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,[],[f3007]) ).
fof(f5577,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,[],[f3114]) ).
fof(f5590,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,[],[f4830]) ).
fof(f5616,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k17_filter_2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3148]) ).
fof(f5621,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,[],[f3154]) ).
fof(f5624,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,[],[f3156]) ).
fof(f5634,plain,
! [X0,X1] :
( m2_filter_2(sK19(X0,X1),X0)
| 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,[],[f4845]) ).
fof(f5635,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| r2_filter_2(X0,sK19(X0,X1))
| ~ m2_filter_2(X1,X0)
| u1_struct_0(X0) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f4845]) ).
fof(f5636,plain,
! [X0,X1] :
( r1_tarski(X1,sK19(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,[],[f4845]) ).
fof(f5638,plain,
l3_lattices(sK20),
inference(cnf_transformation,[],[f4846]) ).
fof(f5639,plain,
v10_lattices(sK20),
inference(cnf_transformation,[],[f4846]) ).
fof(f5640,plain,
~ v3_struct_0(sK20),
inference(cnf_transformation,[],[f4846]) ).
fof(f5641,plain,
m1_subset_1(sK21,u1_struct_0(sK20)),
inference(cnf_transformation,[],[f4846]) ).
fof(f5642,plain,
! [X2] :
( ~ r2_filter_2(sK20,X2)
| ~ r2_hidden(sK21,X2)
| ~ m2_filter_2(X2,sK20) ),
inference(cnf_transformation,[],[f4846]) ).
fof(f5643,plain,
sK21 != k6_lattices(sK20),
inference(cnf_transformation,[],[f4846]) ).
fof(f5644,plain,
v14_lattices(sK20),
inference(cnf_transformation,[],[f4846]) ).
fof(f5717,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,[],[f3220]) ).
fof(f5722,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3226]) ).
fof(f5723,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,[],[f3228]) ).
fof(f5730,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k5_lattices(k8_filter_0(X0,k2_filter_0(X0,X1))) = X1
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3236]) ).
fof(f5799,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f3295]) ).
fof(f5802,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3299]) ).
fof(f5812,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3301]) ).
fof(f6063,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f3468]) ).
fof(f6144,plain,
! [X0] :
( ~ v14_lattices(X0)
| v13_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5025]) ).
fof(f6148,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,[],[f3536]) ).
fof(f6318,plain,
! [X3,X0,X1] :
( ~ r1_tarski(X0,X1)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) ),
inference(cnf_transformation,[],[f5061]) ).
fof(f6505,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f3739]) ).
fof(f6511,plain,
! [X0] :
( ~ l2_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k6_lattices(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f3742]) ).
fof(f8864,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,[],[f5717]) ).
fof(f9113,plain,
! [X0] :
( r2_filter_2(sK20,sK19(sK20,X0))
| ~ m2_filter_2(X0,sK20)
| u1_struct_0(sK20) = X0
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f5635,f5644]) ).
fof(f9114,plain,
! [X0] :
( r2_filter_2(sK20,sK19(sK20,X0))
| ~ m2_filter_2(X0,sK20)
| u1_struct_0(sK20) = X0
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9113,f5640]) ).
fof(f9115,plain,
! [X0] :
( r2_filter_2(sK20,sK19(sK20,X0))
| ~ m2_filter_2(X0,sK20)
| u1_struct_0(sK20) = X0
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9114,f5639]) ).
fof(f9116,plain,
! [X0] :
( r2_filter_2(sK20,sK19(sK20,X0))
| ~ m2_filter_2(X0,sK20)
| u1_struct_0(sK20) = X0 ),
inference(forward_subsumption_resolution,[],[f9115,f5638]) ).
fof(f9117,plain,
( v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| k6_lattices(sK20) = k5_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f6148,f5644]) ).
fof(f9118,plain,
( ~ v10_lattices(sK20)
| k6_lattices(sK20) = k5_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9117,f5640]) ).
fof(f9119,plain,
( k6_lattices(sK20) = k5_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9118,f5639]) ).
fof(f9120,plain,
k6_lattices(sK20) = k5_lattices(k1_lattice2(sK20)),
inference(forward_subsumption_resolution,[],[f9119,f5638]) ).
fof(f9121,plain,
( v3_struct_0(sK20)
| u1_struct_0(sK20) = k17_filter_2(sK20)
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f5616,f5639]) ).
fof(f9122,plain,
( u1_struct_0(sK20) = k17_filter_2(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9121,f5640]) ).
fof(f9123,plain,
u1_struct_0(sK20) = k17_filter_2(sK20),
inference(forward_subsumption_resolution,[],[f9122,f5638]) ).
fof(f9124,plain,
m1_subset_1(sK21,k17_filter_2(sK20)),
inference(superposition,[],[f5641,f9123]) ).
fof(f9126,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| v3_struct_0(sK20)
| r2_hidden(X1,k18_filter_2(sK20,X1))
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f5624,f5639]) ).
fof(f9127,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| r2_hidden(X1,k18_filter_2(sK20,X1))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9126,f5640]) ).
fof(f9128,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| r2_hidden(X1,k18_filter_2(sK20,X1)) ),
inference(forward_subsumption_resolution,[],[f9127,f5638]) ).
fof(f9129,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k17_filter_2(sK20))
| ~ m1_subset_1(X1,u1_struct_0(sK20))
| r2_hidden(X1,k18_filter_2(sK20,X1)) ),
inference(forward_demodulation,[],[f9128,f9123]) ).
fof(f9130,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k17_filter_2(sK20))
| ~ m1_subset_1(X0,k17_filter_2(sK20))
| r2_hidden(X1,k18_filter_2(sK20,X1)) ),
inference(forward_demodulation,[],[f9129,f9123]) ).
fof(f9132,definition,
( spl404_5
<=> ! [X0] : ~ m1_subset_1(X0,k17_filter_2(sK20)) ),
introduced(definition,[new_symbols(definition,[spl404_5])],[avatar_definition]) ).
fof(f9133,plain,
( ! [X0] : ~ m1_subset_1(X0,k17_filter_2(sK20))
| ~ spl404_5 ),
inference(avatar_component_clause,[],[f9132]) ).
fof(f9135,definition,
( spl404_6
<=> ! [X1] :
( ~ m1_subset_1(X1,k17_filter_2(sK20))
| r2_hidden(X1,k18_filter_2(sK20,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl404_6])],[avatar_definition]) ).
fof(f9136,plain,
( ! [X1] :
( ~ m1_subset_1(X1,k17_filter_2(sK20))
| r2_hidden(X1,k18_filter_2(sK20,X1)) )
| ~ spl404_6 ),
inference(avatar_component_clause,[],[f9135]) ).
fof(f9137,plain,
( spl404_5
| spl404_6 ),
inference(avatar_split_clause,[],[f9130,f9135,f9132]) ).
fof(f9138,plain,
( v3_struct_0(sK20)
| u1_struct_0(sK20) = k1_filter_0(sK20)
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f5722,f5639]) ).
fof(f9139,plain,
( u1_struct_0(sK20) = k1_filter_0(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9138,f5640]) ).
fof(f9140,plain,
u1_struct_0(sK20) = k1_filter_0(sK20),
inference(forward_subsumption_resolution,[],[f9139,f5638]) ).
fof(f9142,plain,
k17_filter_2(sK20) = k1_filter_0(sK20),
inference(superposition,[],[f9123,f9140]) ).
fof(f9143,plain,
m1_subset_1(sK21,k1_filter_0(sK20)),
inference(superposition,[],[f5641,f9140]) ).
fof(f9166,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| v3_struct_0(sK20)
| k5_filter_2(sK20,X0) = X0
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f5577,f5639]) ).
fof(f9167,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| k5_filter_2(sK20,X0) = X0
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9166,f5640]) ).
fof(f9168,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| k5_filter_2(sK20,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f9167,f5638]) ).
fof(f9169,plain,
! [X0] :
( ~ m1_subset_1(X0,k17_filter_2(sK20))
| k5_filter_2(sK20,X0) = X0 ),
inference(forward_demodulation,[],[f9168,f9123]) ).
fof(f9171,plain,
! [X0] :
( ~ m2_filter_2(X0,sK20)
| u1_struct_0(sK20) = X0
| ~ r2_hidden(sK21,sK19(sK20,X0))
| ~ m2_filter_2(sK19(sK20,X0),sK20) ),
inference(resolution,[],[f9116,f5642]) ).
fof(f9172,plain,
! [X0] :
( k17_filter_2(sK20) = X0
| ~ m2_filter_2(X0,sK20)
| ~ r2_hidden(sK21,sK19(sK20,X0))
| ~ m2_filter_2(sK19(sK20,X0),sK20) ),
inference(forward_demodulation,[],[f9171,f9123]) ).
fof(f9173,plain,
! [X0] :
( ~ r2_hidden(sK21,sK19(sK20,X0))
| ~ m2_filter_2(X0,sK20)
| k1_filter_0(sK20) = X0
| ~ m2_filter_2(sK19(sK20,X0),sK20) ),
inference(forward_demodulation,[],[f9172,f9142]) ).
fof(f9174,plain,
( $false
| ~ spl404_5 ),
inference(unit_resulting_resolution,[],[f9133,f9124]) ).
fof(f9178,plain,
~ spl404_5,
inference(avatar_contradiction_clause,[],[f9174]) ).
fof(f9179,plain,
( ! [X1] :
( r2_hidden(X1,k18_filter_2(sK20,X1))
| ~ m1_subset_1(X1,k1_filter_0(sK20)) )
| ~ spl404_6 ),
inference(forward_demodulation,[],[f9136,f9142]) ).
fof(f9183,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| k5_filter_2(sK20,X0) = X0 ),
inference(forward_demodulation,[],[f9169,f9142]) ).
fof(f9194,plain,
sK21 = k5_filter_2(sK20,sK21),
inference(resolution,[],[f9183,f9143]) ).
fof(f9229,plain,
( v3_struct_0(sK20)
| u1_struct_0(sK20) = u1_struct_0(k1_lattice2(sK20)) ),
inference(resolution,[],[f6063,f5638]) ).
fof(f9230,plain,
u1_struct_0(sK20) = u1_struct_0(k1_lattice2(sK20)),
inference(forward_subsumption_resolution,[],[f9229,f5640]) ).
fof(f9231,plain,
k17_filter_2(sK20) = u1_struct_0(k1_lattice2(sK20)),
inference(forward_demodulation,[],[f9230,f9123]) ).
fof(f9232,plain,
k1_filter_0(sK20) = u1_struct_0(k1_lattice2(sK20)),
inference(forward_demodulation,[],[f9231,f9142]) ).
fof(f9241,definition,
( spl404_16
<=> v3_struct_0(k1_lattice2(sK20)) ),
introduced(definition,[new_symbols(definition,[spl404_16])],[avatar_definition]) ).
fof(f9242,plain,
( v3_struct_0(k1_lattice2(sK20))
| ~ spl404_16 ),
inference(avatar_component_clause,[],[f9241]) ).
fof(f9247,plain,
l2_lattices(sK20),
inference(resolution,[],[f6505,f5638]) ).
fof(f9248,plain,
( v3_struct_0(sK20)
| m1_subset_1(k6_lattices(sK20),u1_struct_0(sK20)) ),
inference(resolution,[],[f9247,f6511]) ).
fof(f9249,plain,
m1_subset_1(k6_lattices(sK20),u1_struct_0(sK20)),
inference(forward_subsumption_resolution,[],[f9248,f5640]) ).
fof(f9250,plain,
m1_subset_1(k6_lattices(sK20),k17_filter_2(sK20)),
inference(forward_demodulation,[],[f9249,f9123]) ).
fof(f9251,plain,
m1_subset_1(k6_lattices(sK20),k1_filter_0(sK20)),
inference(forward_demodulation,[],[f9250,f9142]) ).
fof(f9253,plain,
k6_lattices(sK20) = k5_filter_2(sK20,k6_lattices(sK20)),
inference(resolution,[],[f9251,f9183]) ).
fof(f9340,definition,
( spl404_26
<=> r2_hidden(sK21,k18_filter_2(sK20,sK21)) ),
introduced(definition,[new_symbols(definition,[spl404_26])],[avatar_definition]) ).
fof(f9341,plain,
( ~ r2_hidden(sK21,k18_filter_2(sK20,sK21))
| spl404_26 ),
inference(avatar_component_clause,[],[f9340]) ).
fof(f9344,plain,
( $false
| spl404_26 ),
inference(unit_resulting_resolution,[],[f5624,f5638,f5639,f5640,f5641,f5641,f9341]) ).
fof(f9349,plain,
spl404_26,
inference(avatar_contradiction_clause,[],[f9344]) ).
fof(f9371,definition,
( spl404_28
<=> r2_hidden(k6_lattices(sK20),k18_filter_2(sK20,k6_lattices(sK20))) ),
introduced(definition,[new_symbols(definition,[spl404_28])],[avatar_definition]) ).
fof(f9372,plain,
( ~ r2_hidden(k6_lattices(sK20),k18_filter_2(sK20,k6_lattices(sK20)))
| spl404_28 ),
inference(avatar_component_clause,[],[f9371]) ).
fof(f9400,plain,
( ~ m1_subset_1(k6_lattices(sK20),k1_filter_0(sK20))
| ~ spl404_6
| spl404_28 ),
inference(resolution,[],[f9372,f9179]) ).
fof(f9405,plain,
( $false
| ~ spl404_6
| spl404_28 ),
inference(forward_subsumption_resolution,[],[f9400,f9251]) ).
fof(f9406,plain,
( ~ spl404_6
| spl404_28 ),
inference(avatar_contradiction_clause,[],[f9405]) ).
fof(f9445,plain,
l3_lattices(k1_lattice2(sK20)),
inference(resolution,[],[f5799,f5638]) ).
fof(f9487,plain,
( v3_struct_0(sK20)
| ~ l3_lattices(sK20)
| ~ spl404_16 ),
inference(resolution,[],[f5812,f9242]) ).
fof(f9489,plain,
( ~ l3_lattices(sK20)
| ~ spl404_16 ),
inference(forward_subsumption_resolution,[],[f9487,f5640]) ).
fof(f9490,plain,
( $false
| ~ spl404_16 ),
inference(forward_subsumption_resolution,[],[f9489,f5638]) ).
fof(f9491,plain,
~ spl404_16,
inference(avatar_contradiction_clause,[],[f9490]) ).
fof(f9500,plain,
( v3_struct_0(sK20)
| v10_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f5802,f5639]) ).
fof(f9502,plain,
( v10_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f9500,f5640]) ).
fof(f9510,plain,
v10_lattices(k1_lattice2(sK20)),
inference(forward_subsumption_resolution,[],[f9502,f5638]) ).
fof(f9542,plain,
! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK20))
| v3_struct_0(k1_lattice2(sK20))
| m1_filter_2(X0,k1_lattice2(sK20))
| ~ l3_lattices(k1_lattice2(sK20)) ),
inference(resolution,[],[f9510,f5477]) ).
fof(f9543,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK20))
| k2_filter_0(k1_lattice2(sK20),X0) = k2_filter_2(k1_lattice2(sK20),X0)
| ~ l3_lattices(k1_lattice2(sK20))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20))) ),
inference(resolution,[],[f9510,f5488]) ).
fof(f9580,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK20))
| k2_filter_0(k1_lattice2(sK20),X0) = k2_filter_2(k1_lattice2(sK20),X0)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20))) ),
inference(forward_subsumption_resolution,[],[f9543,f9445]) ).
fof(f9581,plain,
! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK20))
| v3_struct_0(k1_lattice2(sK20))
| m1_filter_2(X0,k1_lattice2(sK20)) ),
inference(forward_subsumption_resolution,[],[f9542,f9445]) ).
fof(f9612,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| v3_struct_0(k1_lattice2(sK20))
| k2_filter_0(k1_lattice2(sK20),X0) = k2_filter_2(k1_lattice2(sK20),X0) ),
inference(forward_demodulation,[],[f9580,f9232]) ).
fof(f9614,definition,
( spl404_41
<=> ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK20))
| m1_filter_2(X0,k1_lattice2(sK20)) ) ),
introduced(definition,[new_symbols(definition,[spl404_41])],[avatar_definition]) ).
fof(f9615,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK20))
| ~ m1_filter_0(X0,k1_lattice2(sK20)) )
| ~ spl404_41 ),
inference(avatar_component_clause,[],[f9614]) ).
fof(f9616,plain,
( spl404_16
| spl404_41 ),
inference(avatar_split_clause,[],[f9581,f9614,f9241]) ).
fof(f9653,definition,
( spl404_49
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| k2_filter_0(k1_lattice2(sK20),X0) = k2_filter_2(k1_lattice2(sK20),X0) ) ),
introduced(definition,[new_symbols(definition,[spl404_49])],[avatar_definition]) ).
fof(f9654,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| k2_filter_0(k1_lattice2(sK20),X0) = k2_filter_2(k1_lattice2(sK20),X0) )
| ~ spl404_49 ),
inference(avatar_component_clause,[],[f9653]) ).
fof(f9655,plain,
( spl404_16
| spl404_49 ),
inference(avatar_split_clause,[],[f9612,f9653,f9241]) ).
fof(f9807,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20)))
| v3_struct_0(k1_lattice2(sK20))
| k5_lattices(k8_filter_0(k1_lattice2(sK20),k2_filter_0(k1_lattice2(sK20),X0))) = X0
| ~ l3_lattices(k1_lattice2(sK20)) ),
inference(resolution,[],[f5730,f9510]) ).
fof(f9808,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20)))
| v3_struct_0(k1_lattice2(sK20))
| k5_lattices(k8_filter_0(k1_lattice2(sK20),k2_filter_0(k1_lattice2(sK20),X0))) = X0 ),
inference(forward_subsumption_resolution,[],[f9807,f9445]) ).
fof(f9810,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| v3_struct_0(k1_lattice2(sK20))
| k5_lattices(k8_filter_0(k1_lattice2(sK20),k2_filter_0(k1_lattice2(sK20),X0))) = X0 ),
inference(forward_demodulation,[],[f9808,f9232]) ).
fof(f9813,definition,
( spl404_64
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| k5_lattices(k8_filter_0(k1_lattice2(sK20),k2_filter_0(k1_lattice2(sK20),X0))) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl404_64])],[avatar_definition]) ).
fof(f9814,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| k5_lattices(k8_filter_0(k1_lattice2(sK20),k2_filter_0(k1_lattice2(sK20),X0))) = X0 )
| ~ spl404_64 ),
inference(avatar_component_clause,[],[f9813]) ).
fof(f9815,plain,
( spl404_16
| spl404_64 ),
inference(avatar_split_clause,[],[f9810,f9813,f9241]) ).
fof(f9820,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK20))
| m2_filter_2(X0,sK20)
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) )
| ~ spl404_41 ),
inference(resolution,[],[f9615,f5590]) ).
fof(f9822,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK20))
| m2_filter_2(X0,sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) )
| ~ spl404_41 ),
inference(forward_subsumption_resolution,[],[f9820,f5640]) ).
fof(f9823,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK20))
| m2_filter_2(X0,sK20)
| ~ l3_lattices(sK20) )
| ~ spl404_41 ),
inference(forward_subsumption_resolution,[],[f9822,f5639]) ).
fof(f9824,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK20))
| m2_filter_2(X0,sK20) )
| ~ spl404_41 ),
inference(forward_subsumption_resolution,[],[f9823,f5638]) ).
fof(f9871,plain,
( k2_filter_0(k1_lattice2(sK20),sK21) = k2_filter_2(k1_lattice2(sK20),sK21)
| ~ spl404_49 ),
inference(resolution,[],[f9654,f9143]) ).
fof(f9872,plain,
( k2_filter_0(k1_lattice2(sK20),k6_lattices(sK20)) = k2_filter_2(k1_lattice2(sK20),k6_lattices(sK20))
| ~ spl404_49 ),
inference(resolution,[],[f9654,f9251]) ).
fof(f10191,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| v3_struct_0(sK20)
| k18_filter_2(sK20,X0) = k2_filter_2(k1_lattice2(sK20),k5_filter_2(sK20,X0))
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f5621,f5639]) ).
fof(f10194,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| k18_filter_2(sK20,X0) = k2_filter_2(k1_lattice2(sK20),k5_filter_2(sK20,X0))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f10191,f5640]) ).
fof(f10196,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK20))
| k18_filter_2(sK20,X0) = k2_filter_2(k1_lattice2(sK20),k5_filter_2(sK20,X0)) ),
inference(forward_subsumption_resolution,[],[f10194,f5638]) ).
fof(f10201,plain,
! [X0] :
( ~ m1_subset_1(X0,k17_filter_2(sK20))
| k18_filter_2(sK20,X0) = k2_filter_2(k1_lattice2(sK20),k5_filter_2(sK20,X0)) ),
inference(forward_demodulation,[],[f10196,f9123]) ).
fof(f10202,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| k18_filter_2(sK20,X0) = k2_filter_2(k1_lattice2(sK20),k5_filter_2(sK20,X0)) ),
inference(forward_demodulation,[],[f10201,f9142]) ).
fof(f10203,plain,
k18_filter_2(sK20,sK21) = k2_filter_2(k1_lattice2(sK20),k5_filter_2(sK20,sK21)),
inference(resolution,[],[f10202,f9143]) ).
fof(f10204,plain,
k18_filter_2(sK20,k6_lattices(sK20)) = k2_filter_2(k1_lattice2(sK20),k5_filter_2(sK20,k6_lattices(sK20))),
inference(resolution,[],[f10202,f9251]) ).
fof(f10205,plain,
k18_filter_2(sK20,k6_lattices(sK20)) = k2_filter_2(k1_lattice2(sK20),k6_lattices(sK20)),
inference(forward_demodulation,[],[f10204,f9253]) ).
fof(f10206,plain,
k18_filter_2(sK20,sK21) = k2_filter_2(k1_lattice2(sK20),sK21),
inference(forward_demodulation,[],[f10203,f9194]) ).
fof(f10208,plain,
( k18_filter_2(sK20,sK21) = k2_filter_0(k1_lattice2(sK20),sK21)
| ~ spl404_49 ),
inference(superposition,[],[f9871,f10206]) ).
fof(f10211,plain,
( m1_filter_0(k18_filter_2(sK20,sK21),k1_lattice2(sK20))
| v3_struct_0(k1_lattice2(sK20))
| ~ v10_lattices(k1_lattice2(sK20))
| ~ l3_lattices(k1_lattice2(sK20))
| ~ m1_subset_1(sK21,u1_struct_0(k1_lattice2(sK20)))
| ~ spl404_49 ),
inference(superposition,[],[f5723,f10208]) ).
fof(f10212,plain,
( m1_filter_0(k18_filter_2(sK20,sK21),k1_lattice2(sK20))
| v3_struct_0(k1_lattice2(sK20))
| ~ l3_lattices(k1_lattice2(sK20))
| ~ m1_subset_1(sK21,u1_struct_0(k1_lattice2(sK20)))
| ~ spl404_49 ),
inference(forward_subsumption_resolution,[],[f10211,f9510]) ).
fof(f10215,plain,
( m1_filter_0(k18_filter_2(sK20,sK21),k1_lattice2(sK20))
| v3_struct_0(k1_lattice2(sK20))
| ~ m1_subset_1(sK21,u1_struct_0(k1_lattice2(sK20)))
| ~ spl404_49 ),
inference(forward_subsumption_resolution,[],[f10212,f9445]) ).
fof(f10218,plain,
( ~ m1_subset_1(sK21,k1_filter_0(sK20))
| m1_filter_0(k18_filter_2(sK20,sK21),k1_lattice2(sK20))
| v3_struct_0(k1_lattice2(sK20))
| ~ spl404_49 ),
inference(forward_demodulation,[],[f10215,f9232]) ).
fof(f10221,plain,
( m1_filter_0(k18_filter_2(sK20,sK21),k1_lattice2(sK20))
| v3_struct_0(k1_lattice2(sK20))
| ~ spl404_49 ),
inference(forward_subsumption_resolution,[],[f10218,f9143]) ).
fof(f10225,definition,
( spl404_85
<=> m1_filter_0(k18_filter_2(sK20,sK21),k1_lattice2(sK20)) ),
introduced(definition,[new_symbols(definition,[spl404_85])],[avatar_definition]) ).
fof(f10226,plain,
( m1_filter_0(k18_filter_2(sK20,sK21),k1_lattice2(sK20))
| ~ spl404_85 ),
inference(avatar_component_clause,[],[f10225]) ).
fof(f10227,plain,
( spl404_16
| spl404_85
| ~ spl404_49 ),
inference(avatar_split_clause,[],[f10221,f9653,f10225,f9241]) ).
fof(f10236,definition,
( spl404_87
<=> k1_filter_0(sK20) = k18_filter_2(sK20,sK21) ),
introduced(definition,[new_symbols(definition,[spl404_87])],[avatar_definition]) ).
fof(f10237,plain,
( k1_filter_0(sK20) != k18_filter_2(sK20,sK21)
| spl404_87 ),
inference(avatar_component_clause,[],[f10236]) ).
fof(f10243,plain,
( k18_filter_2(sK20,k6_lattices(sK20)) = k2_filter_0(k1_lattice2(sK20),k6_lattices(sK20))
| ~ spl404_49 ),
inference(superposition,[],[f9872,f10205]) ).
fof(f10245,plain,
( m2_filter_2(k18_filter_2(sK20,sK21),sK20)
| ~ spl404_41
| ~ spl404_85 ),
inference(resolution,[],[f10226,f9824]) ).
fof(f10254,plain,
( r2_hidden(sK21,k18_filter_2(sK20,sK21))
| ~ spl404_26 ),
inference(avatar_component_clause,[],[f9340]) ).
fof(f10275,plain,
( k1_filter_0(sK20) = k18_filter_2(sK20,sK21)
| ~ spl404_87 ),
inference(avatar_component_clause,[],[f10236]) ).
fof(f11260,definition,
( spl404_175
<=> k1_filter_0(sK20) = k18_filter_2(sK20,k6_lattices(sK20)) ),
introduced(definition,[new_symbols(definition,[spl404_175])],[avatar_definition]) ).
fof(f11261,plain,
( k1_filter_0(sK20) != k18_filter_2(sK20,k6_lattices(sK20))
| spl404_175 ),
inference(avatar_component_clause,[],[f11260]) ).
fof(f11295,plain,
( k1_filter_0(sK20) = k18_filter_2(sK20,k6_lattices(sK20))
| ~ spl404_175 ),
inference(avatar_component_clause,[],[f11260]) ).
fof(f12728,plain,
( v13_lattices(k1_lattice2(sK20))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f6144,f5644]) ).
fof(f12729,plain,
( v13_lattices(k1_lattice2(sK20))
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f12728,f5640]) ).
fof(f12730,plain,
( v13_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f12729,f5639]) ).
fof(f12731,plain,
v13_lattices(k1_lattice2(sK20)),
inference(forward_subsumption_resolution,[],[f12730,f5638]) ).
fof(f12732,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK20))
| ~ v10_lattices(k1_lattice2(sK20))
| u1_struct_0(k1_lattice2(sK20)) = X0
| ~ l3_lattices(k1_lattice2(sK20))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK20)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK20)) ),
inference(resolution,[],[f12731,f8864]) ).
fof(f12735,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK20))
| u1_struct_0(k1_lattice2(sK20)) = X0
| ~ l3_lattices(k1_lattice2(sK20))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK20)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK20)) ),
inference(forward_subsumption_resolution,[],[f12732,f9510]) ).
fof(f12737,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK20))
| u1_struct_0(k1_lattice2(sK20)) = X0
| ~ r2_hidden(k5_lattices(k1_lattice2(sK20)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK20)) ),
inference(forward_subsumption_resolution,[],[f12735,f9445]) ).
fof(f12739,plain,
! [X0] :
( k1_filter_0(sK20) = X0
| v3_struct_0(k1_lattice2(sK20))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK20)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK20)) ),
inference(forward_demodulation,[],[f12737,f9232]) ).
fof(f12744,plain,
! [X0] :
( ~ r2_hidden(k6_lattices(sK20),X0)
| k1_filter_0(sK20) = X0
| v3_struct_0(k1_lattice2(sK20))
| ~ m1_filter_0(X0,k1_lattice2(sK20)) ),
inference(forward_demodulation,[],[f12739,f9120]) ).
fof(f12746,definition,
( spl404_262
<=> ! [X0] :
( ~ r2_hidden(k6_lattices(sK20),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK20))
| k1_filter_0(sK20) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl404_262])],[avatar_definition]) ).
fof(f12747,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK20))
| ~ r2_hidden(k6_lattices(sK20),X0)
| k1_filter_0(sK20) = X0 )
| ~ spl404_262 ),
inference(avatar_component_clause,[],[f12746]) ).
fof(f12748,plain,
( spl404_16
| spl404_262 ),
inference(avatar_split_clause,[],[f12744,f12746,f9241]) ).
fof(f12751,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),X0))
| k1_filter_0(sK20) = k2_filter_0(k1_lattice2(sK20),X0)
| v3_struct_0(k1_lattice2(sK20))
| ~ v10_lattices(k1_lattice2(sK20))
| ~ l3_lattices(k1_lattice2(sK20))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20))) )
| ~ spl404_262 ),
inference(resolution,[],[f12747,f5723]) ).
fof(f12755,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),X0))
| k1_filter_0(sK20) = k2_filter_0(k1_lattice2(sK20),X0)
| v3_struct_0(k1_lattice2(sK20))
| ~ l3_lattices(k1_lattice2(sK20))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20))) )
| ~ spl404_262 ),
inference(forward_subsumption_resolution,[],[f12751,f9510]) ).
fof(f12756,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),X0))
| k1_filter_0(sK20) = k2_filter_0(k1_lattice2(sK20),X0)
| v3_struct_0(k1_lattice2(sK20))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK20))) )
| ~ spl404_262 ),
inference(forward_subsumption_resolution,[],[f12755,f9445]) ).
fof(f12757,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),X0))
| k1_filter_0(sK20) = k2_filter_0(k1_lattice2(sK20),X0)
| v3_struct_0(k1_lattice2(sK20)) )
| ~ spl404_262 ),
inference(forward_demodulation,[],[f12756,f9232]) ).
fof(f12759,definition,
( spl404_263
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| k1_filter_0(sK20) = k2_filter_0(k1_lattice2(sK20),X0)
| ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl404_263])],[avatar_definition]) ).
fof(f12760,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK20))
| k1_filter_0(sK20) = k2_filter_0(k1_lattice2(sK20),X0)
| ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),X0)) )
| ~ spl404_263 ),
inference(avatar_component_clause,[],[f12759]) ).
fof(f12761,plain,
( spl404_16
| spl404_263
| ~ spl404_262 ),
inference(avatar_split_clause,[],[f12757,f12746,f12759,f9241]) ).
fof(f13046,plain,
( k1_filter_0(sK20) = k2_filter_0(k1_lattice2(sK20),k6_lattices(sK20))
| ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),k6_lattices(sK20)))
| ~ spl404_263 ),
inference(resolution,[],[f12760,f9251]) ).
fof(f13055,plain,
( k1_filter_0(sK20) = k18_filter_2(sK20,k6_lattices(sK20))
| ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),k6_lattices(sK20)))
| ~ spl404_49
| ~ spl404_263 ),
inference(forward_demodulation,[],[f13046,f10243]) ).
fof(f15113,plain,
( ~ r2_hidden(k6_lattices(sK20),k2_filter_0(k1_lattice2(sK20),k6_lattices(sK20)))
| ~ spl404_49
| spl404_175
| ~ spl404_263 ),
inference(forward_subsumption_resolution,[],[f13055,f11261]) ).
fof(f15134,plain,
( ~ r2_hidden(k6_lattices(sK20),k18_filter_2(sK20,k6_lattices(sK20)))
| ~ spl404_49
| spl404_175
| ~ spl404_263 ),
inference(forward_demodulation,[],[f15113,f10243]) ).
fof(f15200,plain,
( ~ spl404_28
| ~ spl404_49
| spl404_175
| ~ spl404_263 ),
inference(avatar_split_clause,[],[f15134,f12759,f11260,f9653,f9371]) ).
fof(f20244,plain,
! [X2,X0,X1] :
( ~ v14_lattices(X2)
| r2_hidden(X0,sK19(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,[],[f6318,f5636]) ).
fof(f20247,plain,
! [X0,X1] :
( r2_hidden(X0,sK19(sK20,X1))
| u1_struct_0(sK20) = X1
| ~ m2_filter_2(X1,sK20)
| ~ r2_hidden(X0,X1)
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f20244,f5644]) ).
fof(f20248,plain,
! [X0,X1] :
( r2_hidden(X0,sK19(sK20,X1))
| u1_struct_0(sK20) = X1
| ~ m2_filter_2(X1,sK20)
| ~ r2_hidden(X0,X1)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f20247,f5640]) ).
fof(f20249,plain,
! [X0,X1] :
( r2_hidden(X0,sK19(sK20,X1))
| u1_struct_0(sK20) = X1
| ~ m2_filter_2(X1,sK20)
| ~ r2_hidden(X0,X1)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f20248,f5639]) ).
fof(f20250,plain,
! [X0,X1] :
( r2_hidden(X0,sK19(sK20,X1))
| u1_struct_0(sK20) = X1
| ~ m2_filter_2(X1,sK20)
| ~ r2_hidden(X0,X1) ),
inference(forward_subsumption_resolution,[],[f20249,f5638]) ).
fof(f20251,plain,
! [X0,X1] :
( k17_filter_2(sK20) = X1
| r2_hidden(X0,sK19(sK20,X1))
| ~ m2_filter_2(X1,sK20)
| ~ r2_hidden(X0,X1) ),
inference(forward_demodulation,[],[f20250,f9123]) ).
fof(f20252,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,sK20)
| r2_hidden(X0,sK19(sK20,X1))
| k1_filter_0(sK20) = X1
| ~ r2_hidden(X0,X1) ),
inference(forward_demodulation,[],[f20251,f9142]) ).
fof(f24396,plain,
( k6_lattices(sK20) = k5_lattices(k8_filter_0(k1_lattice2(sK20),k2_filter_0(k1_lattice2(sK20),k6_lattices(sK20))))
| ~ spl404_64 ),
inference(resolution,[],[f9814,f9251]) ).
fof(f24402,plain,
( sK21 = k5_lattices(k8_filter_0(k1_lattice2(sK20),k2_filter_0(k1_lattice2(sK20),sK21)))
| ~ spl404_64 ),
inference(resolution,[],[f9814,f9143]) ).
fof(f24414,plain,
( sK21 = k5_lattices(k8_filter_0(k1_lattice2(sK20),k18_filter_2(sK20,sK21)))
| ~ spl404_49
| ~ spl404_64 ),
inference(forward_demodulation,[],[f24402,f10208]) ).
fof(f24418,plain,
( k6_lattices(sK20) = k5_lattices(k8_filter_0(k1_lattice2(sK20),k18_filter_2(sK20,k6_lattices(sK20))))
| ~ spl404_49
| ~ spl404_64 ),
inference(forward_demodulation,[],[f24396,f10243]) ).
fof(f24424,plain,
( sK21 = k5_lattices(k8_filter_0(k1_lattice2(sK20),k1_filter_0(sK20)))
| ~ spl404_49
| ~ spl404_64
| ~ spl404_87 ),
inference(forward_demodulation,[],[f24414,f10275]) ).
fof(f24427,plain,
( k6_lattices(sK20) = k5_lattices(k8_filter_0(k1_lattice2(sK20),k1_filter_0(sK20)))
| ~ spl404_49
| ~ spl404_64
| ~ spl404_175 ),
inference(forward_demodulation,[],[f24418,f11295]) ).
fof(f24435,plain,
( sK21 = k6_lattices(sK20)
| ~ spl404_49
| ~ spl404_64
| ~ spl404_87
| ~ spl404_175 ),
inference(forward_demodulation,[],[f24427,f24424]) ).
fof(f24442,plain,
( $false
| ~ spl404_49
| ~ spl404_64
| ~ spl404_87
| ~ spl404_175 ),
inference(forward_subsumption_resolution,[],[f24435,f5643]) ).
fof(f24443,plain,
( ~ spl404_49
| ~ spl404_64
| ~ spl404_87
| ~ spl404_175 ),
inference(avatar_contradiction_clause,[],[f24442]) ).
fof(f30246,definition,
( spl404_1150
<=> r2_hidden(sK21,sK19(sK20,k18_filter_2(sK20,sK21))) ),
introduced(definition,[new_symbols(definition,[spl404_1150])],[avatar_definition]) ).
fof(f30247,plain,
( r2_hidden(sK21,sK19(sK20,k18_filter_2(sK20,sK21)))
| ~ spl404_1150 ),
inference(avatar_component_clause,[],[f30246]) ).
fof(f30411,definition,
( spl404_1174
<=> m2_filter_2(sK19(sK20,k18_filter_2(sK20,sK21)),sK20) ),
introduced(definition,[new_symbols(definition,[spl404_1174])],[avatar_definition]) ).
fof(f30412,plain,
( ~ m2_filter_2(sK19(sK20,k18_filter_2(sK20,sK21)),sK20)
| spl404_1174 ),
inference(avatar_component_clause,[],[f30411]) ).
fof(f30413,plain,
( ~ r2_hidden(sK21,sK19(sK20,k18_filter_2(sK20,sK21)))
| spl404_1150 ),
inference(avatar_component_clause,[],[f30246]) ).
fof(f30415,plain,
( $false
| ~ spl404_26
| ~ spl404_41
| ~ spl404_85
| spl404_87
| spl404_1150 ),
inference(unit_resulting_resolution,[],[f20252,f10254,f10245,f10237,f30413]) ).
fof(f30416,plain,
( ~ spl404_26
| ~ spl404_41
| ~ spl404_85
| spl404_87
| spl404_1150 ),
inference(avatar_contradiction_clause,[],[f30415]) ).
fof(f30417,plain,
( u1_struct_0(sK20) = k18_filter_2(sK20,sK21)
| ~ m2_filter_2(k18_filter_2(sK20,sK21),sK20)
| ~ v14_lattices(sK20)
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| spl404_1174 ),
inference(resolution,[],[f30412,f5634]) ).
fof(f30418,plain,
( u1_struct_0(sK20) = k18_filter_2(sK20,sK21)
| ~ v14_lattices(sK20)
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| ~ spl404_41
| ~ spl404_85
| spl404_1174 ),
inference(forward_subsumption_resolution,[],[f30417,f10245]) ).
fof(f30419,plain,
( u1_struct_0(sK20) = k18_filter_2(sK20,sK21)
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| ~ spl404_41
| ~ spl404_85
| spl404_1174 ),
inference(forward_subsumption_resolution,[],[f30418,f5644]) ).
fof(f30420,plain,
( u1_struct_0(sK20) = k18_filter_2(sK20,sK21)
| ~ v10_lattices(sK20)
| ~ l3_lattices(sK20)
| ~ spl404_41
| ~ spl404_85
| spl404_1174 ),
inference(forward_subsumption_resolution,[],[f30419,f5640]) ).
fof(f30421,plain,
( u1_struct_0(sK20) = k18_filter_2(sK20,sK21)
| ~ l3_lattices(sK20)
| ~ spl404_41
| ~ spl404_85
| spl404_1174 ),
inference(forward_subsumption_resolution,[],[f30420,f5639]) ).
fof(f30422,plain,
( u1_struct_0(sK20) = k18_filter_2(sK20,sK21)
| ~ spl404_41
| ~ spl404_85
| spl404_1174 ),
inference(forward_subsumption_resolution,[],[f30421,f5638]) ).
fof(f30423,plain,
( k17_filter_2(sK20) = k18_filter_2(sK20,sK21)
| ~ spl404_41
| ~ spl404_85
| spl404_1174 ),
inference(forward_demodulation,[],[f30422,f9123]) ).
fof(f30424,plain,
( k1_filter_0(sK20) = k18_filter_2(sK20,sK21)
| ~ spl404_41
| ~ spl404_85
| spl404_1174 ),
inference(forward_demodulation,[],[f30423,f9142]) ).
fof(f30425,plain,
( $false
| ~ spl404_41
| ~ spl404_85
| spl404_87
| spl404_1174 ),
inference(forward_subsumption_resolution,[],[f30424,f10237]) ).
fof(f30426,plain,
( ~ spl404_41
| ~ spl404_85
| spl404_87
| spl404_1174 ),
inference(avatar_contradiction_clause,[],[f30425]) ).
fof(f30427,plain,
( ~ m2_filter_2(k18_filter_2(sK20,sK21),sK20)
| k1_filter_0(sK20) = k18_filter_2(sK20,sK21)
| ~ m2_filter_2(sK19(sK20,k18_filter_2(sK20,sK21)),sK20)
| ~ spl404_1150 ),
inference(resolution,[],[f30247,f9173]) ).
fof(f30429,plain,
( k1_filter_0(sK20) = k18_filter_2(sK20,sK21)
| ~ m2_filter_2(sK19(sK20,k18_filter_2(sK20,sK21)),sK20)
| ~ spl404_41
| ~ spl404_85
| ~ spl404_1150 ),
inference(forward_subsumption_resolution,[],[f30427,f10245]) ).
fof(f30430,plain,
( ~ m2_filter_2(sK19(sK20,k18_filter_2(sK20,sK21)),sK20)
| ~ spl404_41
| ~ spl404_85
| spl404_87
| ~ spl404_1150 ),
inference(forward_subsumption_resolution,[],[f30429,f10237]) ).
fof(f30431,plain,
( ~ spl404_1174
| ~ spl404_41
| ~ spl404_85
| spl404_87
| ~ spl404_1150 ),
inference(avatar_split_clause,[],[f30430,f30246,f10236,f10225,f9614,f30411]) ).
cnf(s3,plain,
( spl404_5
| spl404_6 ),
inference(sat_conversion,[],[f9137]) ).
cnf(s5,plain,
~ spl404_5,
inference(sat_conversion,[],[f9178]) ).
cnf(s15,plain,
spl404_26,
inference(sat_conversion,[],[f9349]) ).
cnf(s22,plain,
( ~ spl404_6
| spl404_28 ),
inference(sat_conversion,[],[f9406]) ).
cnf(s27,plain,
~ spl404_16,
inference(sat_conversion,[],[f9491]) ).
cnf(s38,plain,
( spl404_16
| spl404_41 ),
inference(sat_conversion,[],[f9616]) ).
cnf(s46,plain,
( spl404_16
| spl404_49 ),
inference(sat_conversion,[],[f9655]) ).
cnf(s60,plain,
( spl404_16
| spl404_64 ),
inference(sat_conversion,[],[f9815]) ).
cnf(s83,plain,
( spl404_16
| ~ spl404_49
| spl404_85 ),
inference(sat_conversion,[],[f10227]) ).
cnf(s239,plain,
( spl404_16
| spl404_262 ),
inference(sat_conversion,[],[f12748]) ).
cnf(s240,plain,
( spl404_16
| ~ spl404_262
| spl404_263 ),
inference(sat_conversion,[],[f12761]) ).
cnf(s377,plain,
( ~ spl404_28
| ~ spl404_49
| spl404_175
| ~ spl404_263 ),
inference(sat_conversion,[],[f15200]) ).
cnf(s817,plain,
( ~ spl404_49
| ~ spl404_64
| ~ spl404_87
| ~ spl404_175 ),
inference(sat_conversion,[],[f24443]) ).
cnf(s1184,plain,
( ~ spl404_26
| ~ spl404_41
| ~ spl404_85
| spl404_87
| spl404_1150 ),
inference(sat_conversion,[],[f30416]) ).
cnf(s1185,plain,
( ~ spl404_41
| ~ spl404_85
| spl404_87
| spl404_1174 ),
inference(sat_conversion,[],[f30426]) ).
cnf(s1186,plain,
( ~ spl404_41
| ~ spl404_85
| spl404_87
| ~ spl404_1150
| ~ spl404_1174 ),
inference(sat_conversion,[],[f30431]) ).
cnf(s1256,plain,
spl404_262,
inference(rat,[],[s239,s27]) ).
cnf(s1297,plain,
spl404_64,
inference(rat,[],[s60,s27]) ).
cnf(s1307,plain,
spl404_49,
inference(rat,[],[s46,s27]) ).
cnf(s1315,plain,
spl404_41,
inference(rat,[],[s38,s27]) ).
cnf(s1328,plain,
spl404_263,
inference(rat,[],[s240,s27,s1256]) ).
cnf(s1368,plain,
spl404_85,
inference(rat,[],[s83,s27,s1307]) ).
cnf(s1439,plain,
spl404_6,
inference(rat,[],[s3,s5]) ).
cnf(s1440,plain,
spl404_28,
inference(rat,[],[s22,s1439]) ).
cnf(s1441,plain,
spl404_175,
inference(rat,[],[s377,s1328,s1307,s1440]) ).
cnf(s1450,plain,
~ spl404_87,
inference(rat,[],[s817,s1307,s1297,s1441]) ).
cnf(s1452,plain,
spl404_1174,
inference(rat,[],[s1185,s1368,s1315,s1450]) ).
cnf(s1453,plain,
spl404_1150,
inference(rat,[],[s1184,s15,s1315,s1368,s1450]) ).
cnf(s1464,plain,
$false,
inference(rat,[],[s1186,s1450,s1368,s1315,s1452,s1453]) ).
fof(f30432,plain,
$false,
inference(avatar_sat_refutation,[],[s1464]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT309+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n026.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 14:30:42 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.75/2.87 % (2897157)Detected formulas, will run a generic FOF schedule.
% 12.75/2.87 % (2897163)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=3717481519:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 12.75/2.87 % (2897165)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1866020964:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 12.75/2.87 % (2897164)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=44065813:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 12.75/2.87 % (2897162)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=3370956524:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 12.75/2.87 % (2897165)Refutation not found, incomplete strategy
% 12.75/2.87 % (2897165)------------------------------
% 12.75/2.87 % (2897165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.75/2.87 % (2897165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.75/2.87 % (2897165)CaDiCaL version: 2.1.3
% 12.75/2.87 % (2897165)Termination reason: Refutation not found, incomplete strategy
% 12.75/2.87 % (2897165)Time elapsed: 0.015 s
% 12.75/2.87 % (2897165)Peak memory usage: 91 MB
% 12.75/2.87 % (2897165)Instructions burned: 17 (million)
% 12.75/2.87 % (2897166)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3972123034:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 12.75/2.87 % (2897167)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1825770962:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 12.75/2.87 % (2897168)dis-21_1_sil=8000:lcm=predicate:random_seed=919128734:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 12.75/2.87 % (2897166)Instruction limit reached!
% 12.75/2.87 % (2897166)------------------------------
% 12.75/2.87 % (2897166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.75/2.87 % (2897166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.75/2.87 % (2897166)CaDiCaL version: 2.1.3
% 12.75/2.87 % (2897166)Termination reason: Instruction limit
% 12.75/2.87 % (2897166)Termination phase: Saturation
% 12.75/2.87 % (2897166)Time elapsed: 0.079 s
% 12.75/2.87 % (2897166)Peak memory usage: 92 MB
% 12.75/2.87 % (2897166)Instructions burned: 119 (million)
% 12.75/2.87 % (2897168)Instruction limit reached!
% 12.75/2.87 % (2897168)------------------------------
% 12.75/2.87 % (2897168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.75/2.87 % (2897168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.75/2.87 % (2897168)CaDiCaL version: 2.1.3
% 12.75/2.87 % (2897168)Termination reason: Instruction limit
% 12.75/2.87 % (2897168)Termination phase: Function definition elimination
% 12.75/2.87 % (2897168)Time elapsed: 0.078 s
% 12.75/2.87 % (2897168)Peak memory usage: 93 MB
% 12.75/2.87 % (2897168)Instructions burned: 130 (million)
% 12.75/2.87 % (2897167)Instruction limit reached!
% 12.75/2.87 % (2897167)------------------------------
% 12.75/2.87 % (2897167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.75/2.87 % (2897167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.75/2.87 % (2897167)CaDiCaL version: 2.1.3
% 12.75/2.87 % (2897167)Termination reason: Instruction limit
% 12.75/2.87 % (2897167)Termination phase: Property scanning
% 12.75/2.87 % (2897167)Time elapsed: 0.086 s
% 12.75/2.87 % (2897167)Peak memory usage: 94 MB
% 12.75/2.87 % (2897167)Instructions burned: 140 (million)
% 12.75/2.87 % (2897177)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1652350476:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.75/2.87 % (2897176)lrs+10_1_sil=8000:sp=occurrence:random_seed=902517312:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 12.75/2.87 % (2897178)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2413306776:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 12.75/2.87 % (2897165)------------------------------
% 12.75/2.87 % (2897165)------------------------------
% 12.75/2.87 % (2897177)Instruction limit reached!
% 12.75/2.87 % (2897177)------------------------------
% 12.75/2.87 % (2897177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897177)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897177)Termination reason: Instruction limit
% 13.69/2.94 % (2897177)Termination phase: Saturation
% 13.69/2.94 % (2897177)Time elapsed: 0.081 s
% 13.69/2.94 % (2897177)Peak memory usage: 92 MB
% 13.69/2.94 % (2897177)Instructions burned: 158 (million)
% 13.69/2.94 % (2897182)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=541548682:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 13.69/2.94 % (2897176)Instruction limit reached!
% 13.69/2.94 % (2897176)------------------------------
% 13.69/2.94 % (2897176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897176)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897176)Termination reason: Instruction limit
% 13.69/2.94 % (2897176)Termination phase: Saturation
% 13.69/2.94 % (2897176)Time elapsed: 0.181 s
% 13.69/2.94 % (2897176)Peak memory usage: 94 MB
% 13.69/2.94 % (2897176)Instructions burned: 286 (million)
% 13.69/2.94 % (2897178)Instruction limit reached!
% 13.69/2.94 % (2897178)------------------------------
% 13.69/2.94 % (2897178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897178)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897178)Termination reason: Instruction limit
% 13.69/2.94 % (2897178)Termination phase: Saturation
% 13.69/2.94 % (2897178)Time elapsed: 0.216 s
% 13.69/2.94 % (2897178)Peak memory usage: 95 MB
% 13.69/2.94 % (2897178)Instructions burned: 326 (million)
% 13.69/2.94 % (2897183)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3539577882:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 13.69/2.94 % (2897182)Instruction limit reached!
% 13.69/2.94 % (2897182)------------------------------
% 13.69/2.94 % (2897182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897182)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897182)Termination reason: Instruction limit
% 13.69/2.94 % (2897182)Termination phase: Saturation
% 13.69/2.94 % (2897182)Time elapsed: 0.142 s
% 13.69/2.94 % (2897182)Peak memory usage: 98 MB
% 13.69/2.94 % (2897182)Instructions burned: 249 (million)
% 13.69/2.94 % (2897185)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=589787986:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 13.69/2.94 % (2897187)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1618448895:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 13.69/2.94 % (2897183)Instruction limit reached!
% 13.69/2.94 % (2897183)------------------------------
% 13.69/2.94 % (2897183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897183)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897183)Termination reason: Instruction limit
% 13.69/2.94 % (2897183)Termination phase: Saturation
% 13.69/2.94 % (2897183)Time elapsed: 0.167 s
% 13.69/2.94 % (2897183)Peak memory usage: 95 MB
% 13.69/2.94 % (2897183)Instructions burned: 295 (million)
% 13.69/2.94 % (2897187)Instruction limit reached!
% 13.69/2.94 % (2897187)------------------------------
% 13.69/2.94 % (2897187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897187)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897187)Termination reason: Instruction limit
% 13.69/2.94 % (2897187)Termination phase: Saturation
% 13.69/2.94 % (2897187)Time elapsed: 0.064 s
% 13.69/2.94 % (2897187)Peak memory usage: 93 MB
% 13.69/2.94 % (2897187)Instructions burned: 113 (million)
% 13.69/2.94 % (2897188)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=272861546:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 13.69/2.94 % (2897188)Instruction limit reached!
% 13.69/2.94 % (2897188)------------------------------
% 13.69/2.94 % (2897188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897188)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897188)Termination reason: Instruction limit
% 13.69/2.94 % (2897188)Termination phase: Property scanning
% 13.69/2.94 % (2897188)Time elapsed: 0.076 s
% 13.69/2.94 % (2897188)Peak memory usage: 94 MB
% 13.69/2.94 % (2897188)Instructions burned: 128 (million)
% 13.69/2.94 % (2897191)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1329492490:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 13.69/2.94 % (2897192)lrs+10_1_sil=8000:sp=occurrence:random_seed=3441818765:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 13.69/2.94 % (2897191)Instruction limit reached!
% 13.69/2.94 % (2897191)------------------------------
% 13.69/2.94 % (2897191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897191)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897191)Termination reason: Instruction limit
% 13.69/2.94 % (2897191)Termination phase: Property scanning
% 13.69/2.94 % (2897191)Time elapsed: 0.058 s
% 13.69/2.94 % (2897191)Peak memory usage: 91 MB
% 13.69/2.94 % (2897191)Instructions burned: 117 (million)
% 13.69/2.94 % (2897194)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1705602890:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 13.69/2.94 % (2897197)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1209786592:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 13.69/2.94 % (2897194)Instruction limit reached!
% 13.69/2.94 % (2897194)------------------------------
% 13.69/2.94 % (2897194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897194)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897194)Termination reason: Instruction limit
% 13.69/2.94 % (2897194)Termination phase: Saturation
% 13.69/2.94 % (2897194)Time elapsed: 0.245 s
% 13.69/2.94 % (2897194)Peak memory usage: 95 MB
% 13.69/2.94 % (2897194)Instructions burned: 438 (million)
% 13.69/2.94 % (2897200)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1392373670:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 13.69/2.94 % (2897200)Instruction limit reached!
% 13.69/2.94 % (2897200)------------------------------
% 13.69/2.94 % (2897200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897200)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897200)Termination reason: Instruction limit
% 13.69/2.94 % (2897200)Termination phase: Saturation
% 13.69/2.94 % (2897200)Time elapsed: 0.081 s
% 13.69/2.94 % (2897200)Peak memory usage: 94 MB
% 13.69/2.94 % (2897200)Instructions burned: 135 (million)
% 13.69/2.94 % (2897192)Instruction limit reached!
% 13.69/2.94 % (2897192)------------------------------
% 13.69/2.94 % (2897192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897192)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897192)Termination reason: Instruction limit
% 13.69/2.94 % (2897192)Termination phase: Saturation
% 13.69/2.94 % (2897192)Time elapsed: 0.592 s
% 13.69/2.94 % (2897192)Peak memory usage: 104 MB
% 13.69/2.94 % (2897192)Instructions burned: 907 (million)
% 13.69/2.94 % (2897202)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4227009288:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 13.69/2.94 % (2897203)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2361932735:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 13.69/2.94 % (2897163)First to succeed.
% 13.69/2.94 % (2897163)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2897157"
% 13.69/2.94 % (2897202)Instruction limit reached!
% 13.69/2.94 % (2897202)------------------------------
% 13.69/2.94 % (2897202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/2.94 % (2897202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/2.94 % (2897202)CaDiCaL version: 2.1.3
% 13.69/2.94 % (2897202)Termination reason: Instruction limit
% 13.69/2.94 % (2897202)Termination phase: Saturation
% 13.69/2.94 % (2897202)Time elapsed: 0.296 s
% 13.69/2.94 % (2897202)Peak memory usage: 102 MB
% 13.69/2.94 % (2897202)Instructions burned: 593 (million)
% 13.69/2.94 % (2897163)Refutation found. Thanks to Tanya!
% 13.69/2.94 % SZS status Theorem for theBenchmark
% 13.69/2.94 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/3.14 % (2897163)------------------------------
% 0.17/3.14 % (2897163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/3.14 % (2897163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/3.14 % (2897163)CaDiCaL version: 2.1.3
% 0.17/3.14 % (2897163)Termination reason: Refutation
% 0.17/3.14 % (2897163)Time elapsed: 1.685 s
% 0.17/3.14 % (2897163)Peak memory usage: 170 MB
% 0.17/3.14 % (2897163)Instructions burned: 4643 (million)
% 0.17/3.14 % (2897163)------------------------------
% 0.17/3.14 % (2897163)------------------------------
% 0.17/3.14 % (2897157)Success in time 2.068 s
% 0.17/3.14 % Vampire exiting
%------------------------------------------------------------------------------