%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT307+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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:45 AM UTC 2026
% Result : Theorem 22.74s 4.79s
% Output : Refutation 24.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 32
% Syntax : Number of formulae : 288 ( 43 unt; 12 def)
% Number of atoms : 1105 ( 116 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1358 ( 541 ~; 645 |; 113 &)
% ( 24 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 13 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 2 con; 0-3 aty)
% Number of variables : 207 ( 0 sgn 201 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
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(f8597,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ~ ( X1 != u1_struct_0(X0)
& ! [X2] :
( m1_filter_0(X2,X0)
=> ~ ( r1_tarski(X1,X2)
& v1_filter_0(X2,X0) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t22_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(f9390,axiom,
! [X0] :
( l3_lattices(X0)
=> k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_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(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(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(f12317,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f13529,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_2) ).
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(f13532,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f13561,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f13562,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> k15_filter_2(X0,X1) = k7_filter_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f13582,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_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(f13601,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_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(f13619,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t33_filter_2) ).
fof(f13620,conjecture,
! [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(f13621,negated_conjecture,
~ ! [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) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13620]) ).
fof(f13664,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13529]) ).
fof(f13665,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13664]) ).
fof(f13668,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(f13669,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,[],[f13668]) ).
fof(f13670,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13532]) ).
fof(f13671,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13670]) ).
fof(f13728,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f13561]) ).
fof(f13729,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f13728]) ).
fof(f13730,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f13562]) ).
fof(f13731,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f13730]) ).
fof(f13769,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13582]) ).
fof(f13770,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13769]) ).
fof(f13803,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(f13804,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,[],[f13803]) ).
fof(f13805,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13601]) ).
fof(f13806,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13805]) ).
fof(f13827,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(f13828,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13827]) ).
fof(f13841,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13619]) ).
fof(f13842,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13841]) ).
fof(f13843,plain,
? [X0] :
( ? [X1] :
( X1 != u1_struct_0(X0)
& ! [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,[],[f13621]) ).
fof(f13844,plain,
? [X0] :
( ? [X1] :
( X1 != u1_struct_0(X0)
& ! [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,[],[f13843]) ).
fof(f13855,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12317]) ).
fof(f13856,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13855]) ).
fof(f13897,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(f13898,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13897]) ).
fof(f13953,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(f13954,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13953]) ).
fof(f13963,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(f13964,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,[],[f13963]) ).
fof(f13965,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9390]) ).
fof(f13976,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f13979,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(f13980,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,[],[f13979]) ).
fof(f13981,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(f13982,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13981]) ).
fof(f14350,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ? [X2] :
( r1_tarski(X1,X2)
& v1_filter_0(X2,X0)
& m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8597]) ).
fof(f14351,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ? [X2] :
( r1_tarski(X1,X2)
& v1_filter_0(X2,X0)
& m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14350]) ).
fof(f18173,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,[],[f13669]) ).
fof(f18193,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,[],[f13804]) ).
fof(f18207,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
& ( v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13842]) ).
fof(f18208,plain,
( sK36 != u1_struct_0(sK35)
& ! [X2] :
( ~ r1_tarski(sK36,X2)
| ~ r2_filter_2(sK35,X2)
| ~ m2_filter_2(X2,sK35) )
& m2_filter_2(sK36,sK35)
& v14_lattices(sK35)
& ~ v3_struct_0(sK35)
& v10_lattices(sK35)
& l3_lattices(sK35) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36]),skolemize(X0,sK35),skolemize(X1,sK36)],[f13844]) ).
fof(f18242,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,[],[f13954]) ).
fof(f18436,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ( r1_tarski(X1,sK154(X0,X1))
& v1_filter_0(sK154(X0,X1),X0)
& m1_filter_0(sK154(X0,X1),X0) )
| ~ m1_filter_0(X1,X0) )
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK154]),skolemize(X2,sK154(X0,X1))],[f14351]) ).
fof(f19643,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| m2_lattice4(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13665]) ).
fof(f19646,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| m1_filter_0(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18173]) ).
fof(f19647,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,[],[f18173]) ).
fof(f19648,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| m2_lattice4(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13671]) ).
fof(f19681,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f13729]) ).
fof(f19682,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| k7_filter_2(X0,X1) = k15_filter_2(X0,X1)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f13731]) ).
fof(f19713,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = k1_lattice2(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f13770]) ).
fof(f19759,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,[],[f18193]) ).
fof(f19760,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_filter_2(X1,k1_lattice2(X0))
| v3_struct_0(X0)
| m2_filter_2(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18193]) ).
fof(f19761,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| k7_filter_2(X0,X1) = X1
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13806]) ).
fof(f19786,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k17_filter_2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13828]) ).
fof(f19803,plain,
! [X0,X1] :
( ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18207]) ).
fof(f19804,plain,
l3_lattices(sK35),
inference(cnf_transformation,[],[f18208]) ).
fof(f19805,plain,
v10_lattices(sK35),
inference(cnf_transformation,[],[f18208]) ).
fof(f19806,plain,
~ v3_struct_0(sK35),
inference(cnf_transformation,[],[f18208]) ).
fof(f19807,plain,
v14_lattices(sK35),
inference(cnf_transformation,[],[f18208]) ).
fof(f19808,plain,
m2_filter_2(sK36,sK35),
inference(cnf_transformation,[],[f18208]) ).
fof(f19809,plain,
! [X2] :
( ~ r2_filter_2(sK35,X2)
| ~ r1_tarski(sK36,X2)
| ~ m2_filter_2(X2,sK35) ),
inference(cnf_transformation,[],[f18208]) ).
fof(f19810,plain,
sK36 != u1_struct_0(sK35),
inference(cnf_transformation,[],[f18208]) ).
fof(f19829,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13856]) ).
fof(f19869,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13898]) ).
fof(f19922,plain,
! [X0] :
( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18242]) ).
fof(f19930,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f13964]) ).
fof(f19931,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u2_lattices(X0) = u1_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f13964]) ).
fof(f19932,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f13964]) ).
fof(f19933,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf_transformation,[],[f13965]) ).
fof(f19954,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f13976]) ).
fof(f19957,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13980]) ).
fof(f19967,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13982]) ).
fof(f20512,plain,
! [X0,X1] :
( ~ v13_lattices(X0)
| m1_filter_0(sK154(X0,X1),X0)
| ~ m1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18436]) ).
fof(f20513,plain,
! [X0,X1] :
( v1_filter_0(sK154(X0,X1),X0)
| u1_struct_0(X0) = X1
| ~ m1_filter_0(X1,X0)
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18436]) ).
fof(f20514,plain,
! [X0,X1] :
( ~ v13_lattices(X0)
| r1_tarski(X1,sK154(X0,X1))
| ~ m1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18436]) ).
fof(f28517,plain,
( v3_struct_0(sK35)
| u1_struct_0(sK35) = u1_struct_0(k1_lattice2(sK35)) ),
inference(resolution,[],[f19932,f19804]) ).
fof(f28518,plain,
u1_struct_0(sK35) = u1_struct_0(k1_lattice2(sK35)),
inference(forward_subsumption_resolution,[],[f28517,f19806]) ).
fof(f28519,plain,
( v3_struct_0(sK35)
| u1_struct_0(sK35) = k17_filter_2(sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19786,f19805]) ).
fof(f28520,plain,
( u1_struct_0(sK35) = k17_filter_2(sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28519,f19806]) ).
fof(f28521,plain,
u1_struct_0(sK35) = k17_filter_2(sK35),
inference(forward_subsumption_resolution,[],[f28520,f19804]) ).
fof(f28533,definition,
( spl864_41
<=> v3_struct_0(k1_lattice2(sK35)) ),
introduced(definition,[new_symbols(definition,[spl864_41])],[avatar_definition]) ).
fof(f28534,plain,
( v3_struct_0(k1_lattice2(sK35))
| ~ spl864_41 ),
inference(avatar_component_clause,[],[f28533]) ).
fof(f28539,plain,
( v3_struct_0(sK35)
| u1_struct_0(sK35) = k1_filter_0(sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19869,f19805]) ).
fof(f28540,plain,
( u1_struct_0(sK35) = k1_filter_0(sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28539,f19806]) ).
fof(f28541,plain,
u1_struct_0(sK35) = k1_filter_0(sK35),
inference(forward_subsumption_resolution,[],[f28540,f19804]) ).
fof(f28543,plain,
sK36 != k1_filter_0(sK35),
inference(superposition,[],[f19810,f28541]) ).
fof(f28544,plain,
k17_filter_2(sK35) = k1_filter_0(sK35),
inference(superposition,[],[f28521,f28541]) ).
fof(f28552,plain,
! [X0] :
( v3_struct_0(sK35)
| k7_filter_2(sK35,X0) = k15_filter_2(sK35,X0)
| ~ l3_lattices(sK35)
| ~ m2_filter_2(X0,sK35) ),
inference(resolution,[],[f19682,f19805]) ).
fof(f28553,plain,
! [X0] :
( k7_filter_2(sK35,X0) = k15_filter_2(sK35,X0)
| ~ l3_lattices(sK35)
| ~ m2_filter_2(X0,sK35) ),
inference(forward_subsumption_resolution,[],[f28552,f19806]) ).
fof(f28554,plain,
! [X0] :
( ~ m2_filter_2(X0,sK35)
| k7_filter_2(sK35,X0) = k15_filter_2(sK35,X0) ),
inference(forward_subsumption_resolution,[],[f28553,f19804]) ).
fof(f28555,plain,
k7_filter_2(sK35,sK36) = k15_filter_2(sK35,sK36),
inference(resolution,[],[f28554,f19808]) ).
fof(f28574,plain,
! [X0] :
( ~ m2_filter_2(X0,sK35)
| v3_struct_0(sK35)
| m2_lattice4(X0,sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19648,f19805]) ).
fof(f28575,plain,
! [X0] :
( ~ m2_filter_2(X0,sK35)
| m2_lattice4(X0,sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28574,f19806]) ).
fof(f28576,plain,
! [X0] :
( ~ m2_filter_2(X0,sK35)
| m2_lattice4(X0,sK35) ),
inference(forward_subsumption_resolution,[],[f28575,f19804]) ).
fof(f28577,plain,
m2_lattice4(sK36,sK35),
inference(resolution,[],[f28576,f19808]) ).
fof(f28581,plain,
l3_lattices(k1_lattice2(sK35)),
inference(resolution,[],[f19954,f19804]) ).
fof(f28585,plain,
l3_lattices(k1_lattice2(k1_lattice2(sK35))),
inference(resolution,[],[f28581,f19954]) ).
fof(f28600,plain,
( v3_struct_0(sK35)
| ~ l3_lattices(sK35)
| ~ spl864_41 ),
inference(resolution,[],[f19967,f28534]) ).
fof(f28602,plain,
( ~ l3_lattices(sK35)
| ~ spl864_41 ),
inference(forward_subsumption_resolution,[],[f28600,f19806]) ).
fof(f28603,plain,
( $false
| ~ spl864_41 ),
inference(forward_subsumption_resolution,[],[f28602,f19804]) ).
fof(f28604,plain,
~ spl864_41,
inference(avatar_contradiction_clause,[],[f28603]) ).
fof(f28606,plain,
( v3_struct_0(sK35)
| v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19957,f19805]) ).
fof(f28608,plain,
( v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28606,f19806]) ).
fof(f28613,plain,
v10_lattices(k1_lattice2(sK35)),
inference(forward_subsumption_resolution,[],[f28608,f19804]) ).
fof(f28614,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| m1_filter_0(X0,k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) ),
inference(resolution,[],[f28613,f19646]) ).
fof(f28627,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| m1_filter_0(X0,k1_lattice2(sK35)) ),
inference(forward_subsumption_resolution,[],[f28614,f28581]) ).
fof(f28644,definition,
( spl864_49
<=> ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| m1_filter_0(X0,k1_lattice2(sK35)) ) ),
introduced(definition,[new_symbols(definition,[spl864_49])],[avatar_definition]) ).
fof(f28645,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| m1_filter_0(X0,k1_lattice2(sK35)) )
| ~ spl864_49 ),
inference(avatar_component_clause,[],[f28644]) ).
fof(f28646,plain,
( spl864_41
| spl864_49 ),
inference(avatar_split_clause,[],[f28627,f28644,f28533]) ).
fof(f28693,plain,
( m1_filter_2(k7_filter_2(sK35,sK36),k1_lattice2(sK35))
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ m2_filter_2(sK36,sK35) ),
inference(superposition,[],[f19681,f28555]) ).
fof(f28694,plain,
( m1_filter_2(k7_filter_2(sK35,sK36),k1_lattice2(sK35))
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ m2_filter_2(sK36,sK35) ),
inference(forward_subsumption_resolution,[],[f28693,f19806]) ).
fof(f28696,plain,
( m1_filter_2(k7_filter_2(sK35,sK36),k1_lattice2(sK35))
| ~ l3_lattices(sK35)
| ~ m2_filter_2(sK36,sK35) ),
inference(forward_subsumption_resolution,[],[f28694,f19805]) ).
fof(f28698,plain,
( m1_filter_2(k7_filter_2(sK35,sK36),k1_lattice2(sK35))
| ~ m2_filter_2(sK36,sK35) ),
inference(forward_subsumption_resolution,[],[f28696,f19804]) ).
fof(f28700,plain,
m1_filter_2(k7_filter_2(sK35,sK36),k1_lattice2(sK35)),
inference(forward_subsumption_resolution,[],[f28698,f19808]) ).
fof(f28702,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| v3_struct_0(sK35)
| m2_filter_2(X0,sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19760,f19805]) ).
fof(f28705,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| m2_filter_2(X0,sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28702,f19806]) ).
fof(f28710,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| m2_filter_2(X0,sK35) ),
inference(forward_subsumption_resolution,[],[f28705,f19804]) ).
fof(f28718,plain,
! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| m1_filter_2(X0,k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) ),
inference(resolution,[],[f19647,f28613]) ).
fof(f28719,plain,
! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| m1_filter_2(X0,k1_lattice2(sK35)) ),
inference(forward_subsumption_resolution,[],[f28718,f28581]) ).
fof(f28722,definition,
( spl864_55
<=> ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK35))
| m1_filter_2(X0,k1_lattice2(sK35)) ) ),
introduced(definition,[new_symbols(definition,[spl864_55])],[avatar_definition]) ).
fof(f28723,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35)) )
| ~ spl864_55 ),
inference(avatar_component_clause,[],[f28722]) ).
fof(f28724,plain,
( spl864_41
| spl864_55 ),
inference(avatar_split_clause,[],[f28719,f28722,f28533]) ).
fof(f28727,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK35))
| m2_filter_2(X0,sK35) )
| ~ spl864_55 ),
inference(resolution,[],[f28723,f28710]) ).
fof(f28745,plain,
( m1_subset_1(sK36,k1_zfmisc_1(u1_struct_0(sK35)))
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19829,f28577]) ).
fof(f28746,plain,
( m1_subset_1(sK36,k1_zfmisc_1(u1_struct_0(sK35)))
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28745,f19806]) ).
fof(f28747,plain,
( m1_subset_1(sK36,k1_zfmisc_1(u1_struct_0(sK35)))
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28746,f19805]) ).
fof(f28748,plain,
m1_subset_1(sK36,k1_zfmisc_1(u1_struct_0(sK35))),
inference(forward_subsumption_resolution,[],[f28747,f19804]) ).
fof(f28749,plain,
m1_subset_1(sK36,k1_zfmisc_1(k17_filter_2(sK35))),
inference(forward_demodulation,[],[f28748,f28521]) ).
fof(f28750,plain,
m1_subset_1(sK36,k1_zfmisc_1(k1_filter_0(sK35))),
inference(forward_demodulation,[],[f28749,f28544]) ).
fof(f28753,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35)))
| v3_struct_0(sK35)
| k7_filter_2(sK35,X0) = X0
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19761,f19805]) ).
fof(f28756,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35)))
| k7_filter_2(sK35,X0) = X0
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28753,f19806]) ).
fof(f28758,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35)))
| k7_filter_2(sK35,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f28756,f19804]) ).
fof(f28760,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK35)))
| k7_filter_2(sK35,X0) = X0 ),
inference(forward_demodulation,[],[f28758,f28521]) ).
fof(f28762,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK35)))
| k7_filter_2(sK35,X0) = X0 ),
inference(forward_demodulation,[],[f28760,f28544]) ).
fof(f28767,plain,
sK36 = k7_filter_2(sK35,sK36),
inference(resolution,[],[f28762,f28750]) ).
fof(f28769,plain,
m1_filter_2(sK36,k1_lattice2(sK35)),
inference(superposition,[],[f28700,f28767]) ).
fof(f28772,plain,
( m1_filter_0(sK36,k1_lattice2(sK35))
| ~ spl864_49 ),
inference(resolution,[],[f28769,f28645]) ).
fof(f28778,definition,
( spl864_58
<=> v3_struct_0(k1_lattice2(k1_lattice2(sK35))) ),
introduced(definition,[new_symbols(definition,[spl864_58])],[avatar_definition]) ).
fof(f28779,plain,
( v3_struct_0(k1_lattice2(k1_lattice2(sK35)))
| ~ spl864_58 ),
inference(avatar_component_clause,[],[f28778]) ).
fof(f28862,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| m2_lattice4(X0,k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) ),
inference(resolution,[],[f19643,f28613]) ).
fof(f28863,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| m2_lattice4(X0,k1_lattice2(sK35)) ),
inference(forward_subsumption_resolution,[],[f28862,f28581]) ).
fof(f28866,definition,
( spl864_63
<=> ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| m2_lattice4(X0,k1_lattice2(sK35)) ) ),
introduced(definition,[new_symbols(definition,[spl864_63])],[avatar_definition]) ).
fof(f28867,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK35))
| m2_lattice4(X0,k1_lattice2(sK35)) )
| ~ spl864_63 ),
inference(avatar_component_clause,[],[f28866]) ).
fof(f28868,plain,
( spl864_41
| spl864_63 ),
inference(avatar_split_clause,[],[f28863,f28866,f28533]) ).
fof(f28873,plain,
( ! [X0] :
( m2_lattice4(X0,k1_lattice2(sK35))
| ~ m2_filter_2(X0,sK35)
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35) )
| ~ spl864_63 ),
inference(resolution,[],[f28867,f19759]) ).
fof(f28879,plain,
( ! [X0] :
( m2_lattice4(X0,k1_lattice2(sK35))
| ~ m2_filter_2(X0,sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35) )
| ~ spl864_63 ),
inference(forward_subsumption_resolution,[],[f28873,f19806]) ).
fof(f28881,plain,
( ! [X0] :
( m2_lattice4(X0,k1_lattice2(sK35))
| ~ m2_filter_2(X0,sK35)
| ~ l3_lattices(sK35) )
| ~ spl864_63 ),
inference(forward_subsumption_resolution,[],[f28879,f19805]) ).
fof(f28883,plain,
( ! [X0] :
( m2_lattice4(X0,k1_lattice2(sK35))
| ~ m2_filter_2(X0,sK35) )
| ~ spl864_63 ),
inference(forward_subsumption_resolution,[],[f28881,f19804]) ).
fof(f28890,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK35)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK35))))
| v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) )
| ~ spl864_63 ),
inference(resolution,[],[f28883,f19829]) ).
fof(f28891,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK35)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK35))))
| v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) )
| ~ spl864_63 ),
inference(forward_subsumption_resolution,[],[f28890,f28613]) ).
fof(f28892,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK35)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK35))))
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_63 ),
inference(forward_subsumption_resolution,[],[f28891,f28581]) ).
fof(f28893,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35)))
| ~ m2_filter_2(X0,sK35)
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_63 ),
inference(forward_demodulation,[],[f28892,f28518]) ).
fof(f28894,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK35)))
| ~ m2_filter_2(X0,sK35)
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_63 ),
inference(forward_demodulation,[],[f28893,f28521]) ).
fof(f28895,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK35)))
| ~ m2_filter_2(X0,sK35)
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_63 ),
inference(forward_demodulation,[],[f28894,f28544]) ).
fof(f28897,definition,
( spl864_64
<=> ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK35)))
| ~ m2_filter_2(X0,sK35) ) ),
introduced(definition,[new_symbols(definition,[spl864_64])],[avatar_definition]) ).
fof(f28898,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK35)))
| ~ m2_filter_2(X0,sK35) )
| ~ spl864_64 ),
inference(avatar_component_clause,[],[f28897]) ).
fof(f28899,plain,
( spl864_41
| spl864_64
| ~ spl864_63 ),
inference(avatar_split_clause,[],[f28895,f28866,f28897,f28533]) ).
fof(f28900,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK35)
| k7_filter_2(sK35,X0) = X0 )
| ~ spl864_64 ),
inference(resolution,[],[f28898,f28762]) ).
fof(f28914,definition,
( spl864_65
<=> v13_lattices(k1_lattice2(sK35)) ),
introduced(definition,[new_symbols(definition,[spl864_65])],[avatar_definition]) ).
fof(f28915,plain,
( ~ v13_lattices(k1_lattice2(sK35))
| spl864_65 ),
inference(avatar_component_clause,[],[f28914]) ).
fof(f28921,plain,
( ~ v14_lattices(sK35)
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| spl864_65 ),
inference(resolution,[],[f28915,f19922]) ).
fof(f28923,plain,
( v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| spl864_65 ),
inference(forward_subsumption_resolution,[],[f28921,f19807]) ).
fof(f28924,plain,
( ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| spl864_65 ),
inference(forward_subsumption_resolution,[],[f28923,f19806]) ).
fof(f28925,plain,
( ~ l3_lattices(sK35)
| spl864_65 ),
inference(forward_subsumption_resolution,[],[f28924,f19805]) ).
fof(f28926,plain,
( $false
| spl864_65 ),
inference(forward_subsumption_resolution,[],[f28925,f19804]) ).
fof(f28927,plain,
spl864_65,
inference(avatar_contradiction_clause,[],[f28926]) ).
fof(f29143,plain,
( v3_struct_0(sK35)
| u1_lattices(sK35) = u2_lattices(k1_lattice2(sK35)) ),
inference(resolution,[],[f19930,f19804]) ).
fof(f29149,plain,
u1_lattices(sK35) = u2_lattices(k1_lattice2(sK35)),
inference(forward_subsumption_resolution,[],[f29143,f19806]) ).
fof(f29358,plain,
( v13_lattices(k1_lattice2(sK35))
| ~ spl864_65 ),
inference(avatar_component_clause,[],[f28914]) ).
fof(f29362,plain,
( ! [X0] :
( r1_tarski(X0,sK154(k1_lattice2(sK35),X0))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| u1_struct_0(k1_lattice2(sK35)) = X0
| v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(resolution,[],[f29358,f20514]) ).
fof(f29363,plain,
( ! [X0] :
( r1_tarski(X0,sK154(k1_lattice2(sK35),X0))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| u1_struct_0(k1_lattice2(sK35)) = X0
| v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_subsumption_resolution,[],[f29362,f28613]) ).
fof(f29365,plain,
( ! [X0] :
( r1_tarski(X0,sK154(k1_lattice2(sK35),X0))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| u1_struct_0(k1_lattice2(sK35)) = X0
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_subsumption_resolution,[],[f29363,f28581]) ).
fof(f29367,plain,
( ! [X0] :
( u1_struct_0(sK35) = X0
| r1_tarski(X0,sK154(k1_lattice2(sK35),X0))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_demodulation,[],[f29365,f28518]) ).
fof(f29369,plain,
( ! [X0] :
( k17_filter_2(sK35) = X0
| r1_tarski(X0,sK154(k1_lattice2(sK35),X0))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_demodulation,[],[f29367,f28521]) ).
fof(f29374,plain,
( ! [X0] :
( k1_filter_0(sK35) = X0
| r1_tarski(X0,sK154(k1_lattice2(sK35),X0))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_demodulation,[],[f29369,f28544]) ).
fof(f29376,definition,
( spl864_97
<=> ! [X0] :
( k1_filter_0(sK35) = X0
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| r1_tarski(X0,sK154(k1_lattice2(sK35),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl864_97])],[avatar_definition]) ).
fof(f29377,plain,
( ! [X0] :
( r1_tarski(X0,sK154(k1_lattice2(sK35),X0))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| k1_filter_0(sK35) = X0 )
| ~ spl864_97 ),
inference(avatar_component_clause,[],[f29376]) ).
fof(f29378,plain,
( spl864_41
| spl864_97
| ~ spl864_65 ),
inference(avatar_split_clause,[],[f29374,f28914,f29376,f28533]) ).
fof(f29447,plain,
( v3_struct_0(sK35)
| u2_lattices(sK35) = u1_lattices(k1_lattice2(sK35)) ),
inference(resolution,[],[f19931,f19804]) ).
fof(f29450,plain,
u2_lattices(sK35) = u1_lattices(k1_lattice2(sK35)),
inference(forward_subsumption_resolution,[],[f29447,f19806]) ).
fof(f29500,plain,
( v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(u1_struct_0(k1_lattice2(sK35)),u2_lattices(k1_lattice2(sK35)),u1_lattices(k1_lattice2(sK35))) ),
inference(resolution,[],[f19713,f28581]) ).
fof(f29501,plain,
( v3_struct_0(k1_lattice2(sK35))
| k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(u1_struct_0(k1_lattice2(sK35)),u2_lattices(k1_lattice2(sK35)),u1_lattices(k1_lattice2(sK35))) ),
inference(forward_subsumption_resolution,[],[f29500,f28613]) ).
fof(f29503,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(u1_struct_0(k1_lattice2(sK35)),u2_lattices(k1_lattice2(sK35)),u2_lattices(sK35))
| v3_struct_0(k1_lattice2(sK35)) ),
inference(forward_demodulation,[],[f29501,f29450]) ).
fof(f29505,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(u1_struct_0(k1_lattice2(sK35)),u1_lattices(sK35),u2_lattices(sK35))
| v3_struct_0(k1_lattice2(sK35)) ),
inference(forward_demodulation,[],[f29503,f29149]) ).
fof(f29507,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(u1_struct_0(sK35),u1_lattices(sK35),u2_lattices(sK35))
| v3_struct_0(k1_lattice2(sK35)) ),
inference(forward_demodulation,[],[f29505,f28518]) ).
fof(f29509,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(k17_filter_2(sK35),u1_lattices(sK35),u2_lattices(sK35))
| v3_struct_0(k1_lattice2(sK35)) ),
inference(forward_demodulation,[],[f29507,f28521]) ).
fof(f29510,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(k1_filter_0(sK35),u1_lattices(sK35),u2_lattices(sK35))
| v3_struct_0(k1_lattice2(sK35)) ),
inference(forward_demodulation,[],[f29509,f28544]) ).
fof(f29512,definition,
( spl864_104
<=> k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(k1_filter_0(sK35),u1_lattices(sK35),u2_lattices(sK35)) ),
introduced(definition,[new_symbols(definition,[spl864_104])],[avatar_definition]) ).
fof(f29513,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK35))) = g3_lattices(k1_filter_0(sK35),u1_lattices(sK35),u2_lattices(sK35))
| ~ spl864_104 ),
inference(avatar_component_clause,[],[f29512]) ).
fof(f29514,plain,
( spl864_41
| spl864_104 ),
inference(avatar_split_clause,[],[f29510,f29512,f28533]) ).
fof(f29515,plain,
( v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| ~ spl864_58 ),
inference(resolution,[],[f28779,f19967]) ).
fof(f29516,plain,
( v3_struct_0(k1_lattice2(sK35))
| ~ spl864_58 ),
inference(forward_subsumption_resolution,[],[f29515,f28581]) ).
fof(f29517,plain,
( spl864_41
| ~ spl864_58 ),
inference(avatar_split_clause,[],[f29516,f28778,f28533]) ).
fof(f29759,plain,
( ! [X0] :
( m1_filter_0(sK154(k1_lattice2(sK35),X0),k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| u1_struct_0(k1_lattice2(sK35)) = X0
| v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(resolution,[],[f20512,f29358]) ).
fof(f29760,plain,
( ! [X0] :
( m1_filter_0(sK154(k1_lattice2(sK35),X0),k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| u1_struct_0(k1_lattice2(sK35)) = X0
| v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_subsumption_resolution,[],[f29759,f28613]) ).
fof(f29762,plain,
( ! [X0] :
( m1_filter_0(sK154(k1_lattice2(sK35),X0),k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| u1_struct_0(k1_lattice2(sK35)) = X0
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_subsumption_resolution,[],[f29760,f28581]) ).
fof(f29764,plain,
( ! [X0] :
( u1_struct_0(sK35) = X0
| m1_filter_0(sK154(k1_lattice2(sK35),X0),k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_demodulation,[],[f29762,f28518]) ).
fof(f29766,plain,
( ! [X0] :
( k17_filter_2(sK35) = X0
| m1_filter_0(sK154(k1_lattice2(sK35),X0),k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_demodulation,[],[f29764,f28521]) ).
fof(f29767,plain,
( ! [X0] :
( k1_filter_0(sK35) = X0
| m1_filter_0(sK154(k1_lattice2(sK35),X0),k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35)) )
| ~ spl864_65 ),
inference(forward_demodulation,[],[f29766,f28544]) ).
fof(f29769,definition,
( spl864_131
<=> ! [X0] :
( k1_filter_0(sK35) = X0
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| m1_filter_0(sK154(k1_lattice2(sK35),X0),k1_lattice2(sK35)) ) ),
introduced(definition,[new_symbols(definition,[spl864_131])],[avatar_definition]) ).
fof(f29770,plain,
( ! [X0] :
( m1_filter_0(sK154(k1_lattice2(sK35),X0),k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| k1_filter_0(sK35) = X0 )
| ~ spl864_131 ),
inference(avatar_component_clause,[],[f29769]) ).
fof(f29771,plain,
( spl864_41
| spl864_131
| ~ spl864_65 ),
inference(avatar_split_clause,[],[f29767,f28914,f29769,f28533]) ).
fof(f31236,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK35))
| k1_filter_0(sK35) = X0
| m2_filter_2(sK154(k1_lattice2(sK35),X0),sK35) )
| ~ spl864_55
| ~ spl864_131 ),
inference(resolution,[],[f29770,f28727]) ).
fof(f32223,plain,
( ~ v3_struct_0(k1_lattice2(k1_lattice2(sK35)))
| spl864_58 ),
inference(avatar_component_clause,[],[f28778]) ).
fof(f37266,plain,
k1_lattice2(sK35) = g3_lattices(u1_struct_0(sK35),u1_lattices(sK35),u2_lattices(sK35)),
inference(resolution,[],[f19933,f19804]) ).
fof(f37267,plain,
k1_lattice2(sK35) = g3_lattices(k17_filter_2(sK35),u1_lattices(sK35),u2_lattices(sK35)),
inference(forward_demodulation,[],[f37266,f28521]) ).
fof(f37272,plain,
k1_lattice2(sK35) = g3_lattices(k1_filter_0(sK35),u1_lattices(sK35),u2_lattices(sK35)),
inference(forward_demodulation,[],[f37267,f28544]) ).
fof(f37281,plain,
( k1_lattice2(sK35) = k1_lattice2(k1_lattice2(k1_lattice2(sK35)))
| ~ spl864_104 ),
inference(superposition,[],[f29513,f37272]) ).
fof(f37305,plain,
( ~ v3_struct_0(k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(k1_lattice2(sK35)))
| ~ l3_lattices(k1_lattice2(k1_lattice2(sK35)))
| ~ spl864_104 ),
inference(superposition,[],[f19967,f37281]) ).
fof(f37314,plain,
( ~ v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(k1_lattice2(sK35)))
| spl864_58
| ~ spl864_104 ),
inference(forward_subsumption_resolution,[],[f37305,f32223]) ).
fof(f37337,plain,
( ~ v3_struct_0(k1_lattice2(sK35))
| spl864_58
| ~ spl864_104 ),
inference(forward_subsumption_resolution,[],[f37314,f28585]) ).
fof(f47420,plain,
( sK36 = k1_filter_0(sK35)
| m2_filter_2(sK154(k1_lattice2(sK35),sK36),sK35)
| ~ spl864_49
| ~ spl864_55
| ~ spl864_131 ),
inference(resolution,[],[f31236,f28772]) ).
fof(f47439,plain,
( m2_filter_2(sK154(k1_lattice2(sK35),sK36),sK35)
| ~ spl864_49
| ~ spl864_55
| ~ spl864_131 ),
inference(forward_subsumption_resolution,[],[f47420,f28543]) ).
fof(f47454,plain,
( k7_filter_2(sK35,sK154(k1_lattice2(sK35),sK36)) = k15_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| ~ spl864_49
| ~ spl864_55
| ~ spl864_131 ),
inference(resolution,[],[f47439,f28554]) ).
fof(f47457,plain,
( sK154(k1_lattice2(sK35),sK36) = k7_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131 ),
inference(resolution,[],[f47439,f28900]) ).
fof(f47498,definition,
( spl864_1512
<=> r2_filter_2(sK35,sK154(k1_lattice2(sK35),sK36)) ),
introduced(definition,[new_symbols(definition,[spl864_1512])],[avatar_definition]) ).
fof(f47499,plain,
( r2_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| ~ spl864_1512 ),
inference(avatar_component_clause,[],[f47498]) ).
fof(f47513,definition,
( spl864_1516
<=> v1_filter_0(sK154(k1_lattice2(sK35),sK36),k1_lattice2(sK35)) ),
introduced(definition,[new_symbols(definition,[spl864_1516])],[avatar_definition]) ).
fof(f47557,plain,
( sK154(k1_lattice2(sK35),sK36) = k15_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131 ),
inference(forward_demodulation,[],[f47454,f47457]) ).
fof(f47564,plain,
( ~ r1_tarski(sK36,sK154(k1_lattice2(sK35),sK36))
| ~ m2_filter_2(sK154(k1_lattice2(sK35),sK36),sK35)
| ~ spl864_1512 ),
inference(resolution,[],[f47499,f19809]) ).
fof(f47569,plain,
( ~ r1_tarski(sK36,sK154(k1_lattice2(sK35),sK36))
| ~ spl864_49
| ~ spl864_55
| ~ spl864_131
| ~ spl864_1512 ),
inference(forward_subsumption_resolution,[],[f47564,f47439]) ).
fof(f47592,plain,
( ~ m1_filter_0(sK36,k1_lattice2(sK35))
| sK36 = k1_filter_0(sK35)
| ~ spl864_49
| ~ spl864_55
| ~ spl864_97
| ~ spl864_131
| ~ spl864_1512 ),
inference(resolution,[],[f47569,f29377]) ).
fof(f47596,plain,
( sK36 = k1_filter_0(sK35)
| ~ spl864_49
| ~ spl864_55
| ~ spl864_97
| ~ spl864_131
| ~ spl864_1512 ),
inference(forward_subsumption_resolution,[],[f47592,f28772]) ).
fof(f47598,plain,
( $false
| ~ spl864_49
| ~ spl864_55
| ~ spl864_97
| ~ spl864_131
| ~ spl864_1512 ),
inference(forward_subsumption_resolution,[],[f47596,f28543]) ).
fof(f47599,plain,
( ~ spl864_49
| ~ spl864_55
| ~ spl864_97
| ~ spl864_131
| ~ spl864_1512 ),
inference(avatar_contradiction_clause,[],[f47598]) ).
fof(f47776,plain,
( ~ v1_filter_0(sK154(k1_lattice2(sK35),sK36),k1_lattice2(sK35))
| r2_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| ~ m2_filter_2(sK154(k1_lattice2(sK35),sK36),sK35)
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131 ),
inference(superposition,[],[f19803,f47557]) ).
fof(f47783,plain,
( ~ v1_filter_0(sK154(k1_lattice2(sK35),sK36),k1_lattice2(sK35))
| r2_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131 ),
inference(forward_subsumption_resolution,[],[f47776,f47439]) ).
fof(f47784,plain,
( ~ v1_filter_0(sK154(k1_lattice2(sK35),sK36),k1_lattice2(sK35))
| r2_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131 ),
inference(forward_subsumption_resolution,[],[f47783,f19806]) ).
fof(f47785,plain,
( ~ v1_filter_0(sK154(k1_lattice2(sK35),sK36),k1_lattice2(sK35))
| r2_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| ~ l3_lattices(sK35)
| ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131 ),
inference(forward_subsumption_resolution,[],[f47784,f19805]) ).
fof(f47786,plain,
( ~ v1_filter_0(sK154(k1_lattice2(sK35),sK36),k1_lattice2(sK35))
| r2_filter_2(sK35,sK154(k1_lattice2(sK35),sK36))
| ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131 ),
inference(forward_subsumption_resolution,[],[f47785,f19804]) ).
fof(f47787,plain,
( ~ v1_filter_0(sK154(k1_lattice2(sK35),sK36),k1_lattice2(sK35))
| spl864_1516 ),
inference(avatar_component_clause,[],[f47513]) ).
fof(f47788,plain,
( spl864_1512
| ~ spl864_1516
| ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131 ),
inference(avatar_split_clause,[],[f47786,f29769,f28897,f28722,f28644,f47513,f47498]) ).
fof(f47789,plain,
( sK36 = u1_struct_0(k1_lattice2(sK35))
| ~ m1_filter_0(sK36,k1_lattice2(sK35))
| ~ v13_lattices(k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| spl864_1516 ),
inference(resolution,[],[f47787,f20513]) ).
fof(f47790,plain,
( sK36 = u1_struct_0(k1_lattice2(sK35))
| ~ v13_lattices(k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| ~ spl864_49
| spl864_1516 ),
inference(forward_subsumption_resolution,[],[f47789,f28772]) ).
fof(f47791,plain,
( sK36 = u1_struct_0(k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| ~ spl864_49
| ~ spl864_65
| spl864_1516 ),
inference(forward_subsumption_resolution,[],[f47790,f29358]) ).
fof(f47792,plain,
( sK36 = u1_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| ~ spl864_49
| spl864_58
| ~ spl864_65
| ~ spl864_104
| spl864_1516 ),
inference(forward_subsumption_resolution,[],[f47791,f37337]) ).
fof(f47793,plain,
( sK36 = u1_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| ~ spl864_49
| spl864_58
| ~ spl864_65
| ~ spl864_104
| spl864_1516 ),
inference(forward_subsumption_resolution,[],[f47792,f28613]) ).
fof(f47794,plain,
( sK36 = u1_struct_0(k1_lattice2(sK35))
| ~ spl864_49
| spl864_58
| ~ spl864_65
| ~ spl864_104
| spl864_1516 ),
inference(forward_subsumption_resolution,[],[f47793,f28581]) ).
fof(f47795,plain,
( sK36 = u1_struct_0(sK35)
| ~ spl864_49
| spl864_58
| ~ spl864_65
| ~ spl864_104
| spl864_1516 ),
inference(superposition,[],[f47794,f28518]) ).
fof(f47852,plain,
( $false
| ~ spl864_49
| spl864_58
| ~ spl864_65
| ~ spl864_104
| spl864_1516 ),
inference(forward_subsumption_resolution,[],[f47795,f19810]) ).
fof(f47853,plain,
( ~ spl864_49
| spl864_58
| ~ spl864_65
| ~ spl864_104
| spl864_1516 ),
inference(avatar_contradiction_clause,[],[f47852]) ).
cnf(s40,plain,
~ spl864_41,
inference(sat_conversion,[],[f28604]) ).
cnf(s46,plain,
( spl864_41
| spl864_49 ),
inference(sat_conversion,[],[f28646]) ).
cnf(s52,plain,
( spl864_41
| spl864_55 ),
inference(sat_conversion,[],[f28724]) ).
cnf(s59,plain,
( spl864_41
| spl864_63 ),
inference(sat_conversion,[],[f28868]) ).
cnf(s60,plain,
( spl864_41
| ~ spl864_63
| spl864_64 ),
inference(sat_conversion,[],[f28899]) ).
cnf(s63,plain,
spl864_65,
inference(sat_conversion,[],[f28927]) ).
cnf(s87,plain,
( spl864_41
| ~ spl864_65
| spl864_97 ),
inference(sat_conversion,[],[f29378]) ).
cnf(s94,plain,
( spl864_41
| spl864_104 ),
inference(sat_conversion,[],[f29514]) ).
cnf(s95,plain,
( spl864_41
| ~ spl864_58 ),
inference(sat_conversion,[],[f29517]) ).
cnf(s122,plain,
( spl864_41
| ~ spl864_65
| spl864_131 ),
inference(sat_conversion,[],[f29771]) ).
cnf(s1474,plain,
( ~ spl864_49
| ~ spl864_55
| ~ spl864_97
| ~ spl864_131
| ~ spl864_1512 ),
inference(sat_conversion,[],[f47599]) ).
cnf(s1481,plain,
( ~ spl864_49
| ~ spl864_55
| ~ spl864_64
| ~ spl864_131
| spl864_1512
| ~ spl864_1516 ),
inference(sat_conversion,[],[f47788]) ).
cnf(s1483,plain,
( ~ spl864_49
| spl864_58
| ~ spl864_65
| ~ spl864_104
| spl864_1516 ),
inference(sat_conversion,[],[f47853]) ).
cnf(s1835,plain,
spl864_131,
inference(rat,[],[s122,s63,s40]) ).
cnf(s1839,plain,
~ spl864_58,
inference(rat,[],[s95,s40]) ).
cnf(s1840,plain,
spl864_104,
inference(rat,[],[s94,s40]) ).
cnf(s1846,plain,
spl864_97,
inference(rat,[],[s87,s63,s40]) ).
cnf(s1855,plain,
spl864_63,
inference(rat,[],[s59,s40]) ).
cnf(s1860,plain,
spl864_55,
inference(rat,[],[s52,s40]) ).
cnf(s1865,plain,
spl864_49,
inference(rat,[],[s46,s40]) ).
cnf(s1896,plain,
spl864_64,
inference(rat,[],[s60,s40,s1855]) ).
cnf(s1905,plain,
spl864_1516,
inference(rat,[],[s1483,s1839,s1840,s63,s1865]) ).
cnf(s1906,plain,
spl864_1512,
inference(rat,[],[s1481,s1905,s1860,s1835,s1896,s1865]) ).
cnf(s1907,plain,
$false,
inference(rat,[],[s1474,s1860,s1835,s1846,s1906,s1865]) ).
fof(f47935,plain,
$false,
inference(avatar_sat_refutation,[],[s1907]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT307+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 % Computer : n014.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 14:26:49 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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
% 15.90/3.81 % (865118)Detected formulas, will run a generic FOF schedule.
% 15.90/3.81 % (865128)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=842070991:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 15.90/3.81 % (865124)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=3134351327:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 15.90/3.81 % (865125)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=3678646421:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 15.90/3.81 % (865123)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=3503254302:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 15.90/3.81 % (865128)Instruction limit reached!
% 15.90/3.81 % (865128)------------------------------
% 15.90/3.81 % (865128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.81 % (865128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.81 % (865128)CaDiCaL version: 2.1.3
% 15.90/3.81 % (865128)Termination reason: Instruction limit
% 15.90/3.81 % (865128)Termination phase: Property scanning
% 15.90/3.81 % (865128)Time elapsed: 0.034 s
% 15.90/3.81 % (865128)Peak memory usage: 103 MB
% 15.90/3.81 % (865128)Instructions burned: 142 (million)
% 15.90/3.81 % (865126)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2933936056:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 15.90/3.81 % (865129)dis-21_1_sil=8000:lcm=predicate:random_seed=587612576: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)
% 15.90/3.81 % (865127)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3638195830:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 15.90/3.81 % (865126)Refutation not found, incomplete strategy
% 15.90/3.81 % (865126)------------------------------
% 15.90/3.81 % (865126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.81 % (865126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.81 % (865126)CaDiCaL version: 2.1.3
% 15.90/3.81 % (865126)Termination reason: Refutation not found, incomplete strategy
% 15.90/3.81 % (865126)Time elapsed: 0.067 s
% 15.90/3.81 % (865126)Peak memory usage: 107 MB
% 15.90/3.81 % (865126)Instructions burned: 86 (million)
% 15.90/3.81 % (865127)Instruction limit reached!
% 15.90/3.81 % (865127)------------------------------
% 15.90/3.81 % (865127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.81 % (865127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.81 % (865127)CaDiCaL version: 2.1.3
% 15.90/3.81 % (865127)Termination reason: Instruction limit
% 15.90/3.81 % (865127)Termination phase: Function definition elimination
% 15.90/3.81 % (865127)Time elapsed: 0.090 s
% 15.90/3.81 % (865127)Peak memory usage: 105 MB
% 15.90/3.81 % (865127)Instructions burned: 121 (million)
% 15.90/3.81 % (865129)Instruction limit reached!
% 15.90/3.81 % (865129)------------------------------
% 15.90/3.81 % (865129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.81 % (865129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.81 % (865129)CaDiCaL version: 2.1.3
% 15.90/3.81 % (865129)Termination reason: Instruction limit
% 15.90/3.81 % (865129)Termination phase: Preprocessing 1
% 15.90/3.81 % (865129)Time elapsed: 0.096 s
% 15.90/3.81 % (865129)Peak memory usage: 103 MB
% 15.90/3.81 % (865129)Instructions burned: 130 (million)
% 15.90/3.81 % (865137)lrs+10_1_sil=8000:sp=occurrence:random_seed=3373820072:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 15.90/3.81 % (865138)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3673724625:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 15.90/3.81 % (865139)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4148079274:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 15.90/3.81 % (865126)------------------------------
% 15.90/3.81 % (865126)------------------------------
% 15.90/3.81 % (865137)Instruction limit reached!
% 15.90/3.81 % (865137)------------------------------
% 15.90/3.81 % (865137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865137)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865137)Termination reason: Instruction limit
% 22.74/4.79 % (865137)Termination phase: Saturation
% 22.74/4.79 % (865137)Time elapsed: 0.169 s
% 22.74/4.79 % (865137)Peak memory usage: 110 MB
% 22.74/4.79 % (865137)Instructions burned: 286 (million)
% 22.74/4.79 % (865138)Instruction limit reached!
% 22.74/4.79 % (865138)------------------------------
% 22.74/4.79 % (865138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865138)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865138)Termination reason: Instruction limit
% 22.74/4.79 % (865138)Termination phase: Property scanning
% 22.74/4.79 % (865138)Time elapsed: 0.067 s
% 22.74/4.79 % (865138)Peak memory usage: 102 MB
% 22.74/4.79 % (865138)Instructions burned: 159 (million)
% 22.74/4.79 % (865144)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1922013921:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 22.74/4.79 % (865145)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=912165385:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 22.74/4.79 % (865143)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=3415650926:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 22.74/4.79 % (865139)Instruction limit reached!
% 22.74/4.79 % (865139)------------------------------
% 22.74/4.79 % (865139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865139)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865139)Termination reason: Instruction limit
% 22.74/4.79 % (865139)Termination phase: Saturation
% 22.74/4.79 % (865139)Time elapsed: 0.245 s
% 22.74/4.79 % (865139)Peak memory usage: 109 MB
% 22.74/4.79 % (865139)Instructions burned: 326 (million)
% 22.74/4.79 % (865144)Refutation not found, incomplete strategy
% 22.74/4.79 % (865144)------------------------------
% 22.74/4.79 % (865144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865144)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865144)Termination reason: Refutation not found, incomplete strategy
% 22.74/4.79 % (865144)Time elapsed: 0.093 s
% 22.74/4.79 % (865144)Peak memory usage: 110 MB
% 22.74/4.79 % (865144)Instructions burned: 256 (million)
% 22.74/4.79 % (865143)Instruction limit reached!
% 22.74/4.79 % (865143)------------------------------
% 22.74/4.79 % (865143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865143)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865143)Termination reason: Instruction limit
% 22.74/4.79 % (865143)Termination phase: SInE selection
% 22.74/4.79 % (865143)Time elapsed: 0.131 s
% 22.74/4.79 % (865143)Peak memory usage: 103 MB
% 22.74/4.79 % (865143)Instructions burned: 249 (million)
% 22.74/4.79 % (865149)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4026250622:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 22.74/4.79 % (865144)------------------------------
% 22.74/4.79 % (865144)------------------------------
% 22.74/4.79 % (865150)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2796833414:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 22.74/4.79 % (865149)Instruction limit reached!
% 22.74/4.79 % (865149)------------------------------
% 22.74/4.79 % (865149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865149)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865149)Termination reason: Instruction limit
% 22.74/4.79 % (865149)Termination phase: Preprocessing 3
% 22.74/4.79 % (865149)Time elapsed: 0.097 s
% 22.74/4.79 % (865149)Peak memory usage: 105 MB
% 22.74/4.79 % (865149)Instructions burned: 113 (million)
% 22.74/4.79 % (865152)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3978851162:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 22.74/4.79 % (865152)Instruction limit reached!
% 22.74/4.79 % (865152)------------------------------
% 22.74/4.79 % (865152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865152)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865152)Termination reason: Instruction limit
% 22.74/4.79 % (865152)Termination phase: Property scanning
% 22.74/4.79 % (865152)Time elapsed: 0.027 s
% 22.74/4.79 % (865152)Peak memory usage: 103 MB
% 22.74/4.79 % (865152)Instructions burned: 115 (million)
% 22.74/4.79 % (865150)Instruction limit reached!
% 22.74/4.79 % (865150)------------------------------
% 22.74/4.79 % (865150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865150)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865150)Termination reason: Instruction limit
% 22.74/4.79 % (865150)Termination phase: Preprocessing 2
% 22.74/4.79 % (865150)Time elapsed: 0.102 s
% 22.74/4.79 % (865150)Peak memory usage: 106 MB
% 22.74/4.79 % (865150)Instructions burned: 127 (million)
% 22.74/4.79 % (865154)lrs+10_1_sil=8000:sp=occurrence:random_seed=1077240631:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 22.74/4.79 % (865156)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3386937920:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 22.74/4.79 % (865157)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3612546400:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 22.74/4.79 % (865156)Refutation not found, incomplete strategy
% 22.74/4.79 % (865156)------------------------------
% 22.74/4.79 % (865156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865156)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865156)Termination reason: Refutation not found, incomplete strategy
% 22.74/4.79 % (865156)Time elapsed: 0.093 s
% 22.74/4.79 % (865156)Peak memory usage: 108 MB
% 22.74/4.79 % (865156)Instructions burned: 124 (million)
% 22.74/4.79 % (865156)------------------------------
% 22.74/4.79 % (865156)------------------------------
% 22.74/4.79 % (865154)Instruction limit reached!
% 22.74/4.79 % (865154)------------------------------
% 22.74/4.79 % (865154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865154)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865154)Termination reason: Instruction limit
% 22.74/4.79 % (865154)Termination phase: Saturation
% 22.74/4.79 % (865154)Time elapsed: 0.584 s
% 22.74/4.79 % (865154)Peak memory usage: 122 MB
% 22.74/4.79 % (865154)Instructions burned: 908 (million)
% 22.74/4.79 % (865161)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2957494719:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2977 on theBenchmark for (2977ds/134Mi)
% 22.74/4.79 % (865161)Instruction limit reached!
% 22.74/4.79 % (865161)------------------------------
% 22.74/4.79 % (865161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865161)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865161)Termination reason: Instruction limit
% 22.74/4.79 % (865161)Termination phase: Property scanning
% 22.74/4.79 % (865161)Time elapsed: 0.100 s
% 22.74/4.79 % (865161)Peak memory usage: 106 MB
% 22.74/4.79 % (865161)Instructions burned: 134 (million)
% 22.74/4.79 % (865162)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3143302320:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 22.74/4.79 % (865164)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2264876826:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 22.74/4.79 % (865145)Instruction limit reached!
% 22.74/4.79 % (865145)------------------------------
% 22.74/4.79 % (865145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865145)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865145)Termination reason: Instruction limit
% 22.74/4.79 % (865145)Termination phase: Saturation
% 22.74/4.79 % (865145)Time elapsed: 1.427 s
% 22.74/4.79 % (865145)Peak memory usage: 239 MB
% 22.74/4.79 % (865145)Instructions burned: 2351 (million)
% 22.74/4.79 % (865167)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=2537433631:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 22.74/4.79 % (865162)Instruction limit reached!
% 22.74/4.79 % (865162)------------------------------
% 22.74/4.79 % (865162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865162)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865162)Termination reason: Instruction limit
% 22.74/4.79 % (865162)Termination phase: Property scanning
% 22.74/4.79 % (865162)Time elapsed: 0.415 s
% 22.74/4.79 % (865162)Peak memory usage: 124 MB
% 22.74/4.79 % (865162)Instructions burned: 594 (million)
% 22.74/4.79 % (865167)Instruction limit reached!
% 22.74/4.79 % (865167)------------------------------
% 22.74/4.79 % (865167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865167)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865167)Termination reason: Instruction limit
% 22.74/4.79 % (865167)Termination phase: Property scanning
% 22.74/4.79 % (865167)Time elapsed: 0.054 s
% 22.74/4.79 % (865167)Peak memory usage: 103 MB
% 22.74/4.79 % (865167)Instructions burned: 126 (million)
% 22.74/4.79 % (865169)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1827418776:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 22.74/4.79 % (865170)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2760854838:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/141Mi)
% 22.74/4.79 % (865169)Instruction limit reached!
% 22.74/4.79 % (865169)------------------------------
% 22.74/4.79 % (865169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865169)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865169)Termination reason: Instruction limit
% 22.74/4.79 % (865169)Termination phase: Property scanning
% 22.74/4.79 % (865169)Time elapsed: 0.059 s
% 22.74/4.79 % (865169)Peak memory usage: 103 MB
% 22.74/4.79 % (865169)Instructions burned: 135 (million)
% 22.74/4.79 % (865170)Instruction limit reached!
% 22.74/4.79 % (865170)------------------------------
% 22.74/4.79 % (865170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865170)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865170)Termination reason: Instruction limit
% 22.74/4.79 % (865170)Termination phase: Saturation
% 22.74/4.79 % (865170)Time elapsed: 0.103 s
% 22.74/4.79 % (865170)Peak memory usage: 107 MB
% 22.74/4.79 % (865170)Instructions burned: 141 (million)
% 22.74/4.79 % (865173)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=204691734:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 22.74/4.79 % (865174)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=2448544751:i=6060:aac=none:ins=25_2967 on theBenchmark for (2967ds/6060Mi)
% 22.74/4.79 % (865173)Instruction limit reached!
% 22.74/4.79 % (865173)------------------------------
% 22.74/4.79 % (865173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/4.79 % (865173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/4.79 % (865173)CaDiCaL version: 2.1.3
% 22.74/4.79 % (865173)Termination reason: Instruction limit
% 22.74/4.79 % (865173)Termination phase: Saturation
% 22.74/4.79 % (865173)Time elapsed: 0.279 s
% 22.74/4.79 % (865173)Peak memory usage: 111 MB
% 22.74/4.79 % (865173)Instructions burned: 431 (million)
% 22.74/4.79 % (865124)First to succeed.
% 22.74/4.79 % (865124)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-865118"
% 22.74/4.79 % (865177)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=3797493746:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2963 on theBenchmark for (2963ds/150Mi)
% 22.74/4.79 % (865124)Refutation found. Thanks to Tanya!
% 22.74/4.79 % SZS status Theorem for theBenchmark
% 22.74/4.79 % SZS output start Proof for theBenchmark
% See solution above
% 24.06/5.00 % (865124)------------------------------
% 24.06/5.00 % (865124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/5.00 % (865124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/5.00 % (865124)CaDiCaL version: 2.1.3
% 24.06/5.00 % (865124)Termination reason: Refutation
% 24.06/5.00 % (865124)Time elapsed: 2.864 s
% 24.06/5.00 % (865124)Peak memory usage: 230 MB
% 24.06/5.00 % (865124)Instructions burned: 6673 (million)
% 24.06/5.00 % (865124)------------------------------
% 24.06/5.00 % (865124)------------------------------
% 24.06/5.00 % (865118)Success in time 3.928 s
% 24.06/5.00 % Vampire exiting
%------------------------------------------------------------------------------