%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT317+3 : 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 : n013.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:52 AM UTC 2026
% Result : Theorem 18.54s 4.46s
% Output : Refutation 21.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 25
% Syntax : Number of formulae : 194 ( 37 unt; 11 def)
% Number of atoms : 753 ( 68 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 902 ( 343 ~; 417 |; 100 &)
% ( 14 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 12 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-3 aty)
% Number of variables : 169 ( 0 sgn 163 !; 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/sandbox2/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f8627,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ! [X2] :
( m1_filter_0(X2,X0)
=> ( r1_tarski(X1,k5_filter_0(X0,X1,X2))
& r1_tarski(X2,k5_filter_0(X0,X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t49_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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9391,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f9463,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(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/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f13532,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(f13533,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/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f13562,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/sandbox2/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f13563,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/sandbox2/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f13602,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/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f13638,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X3] :
( ( ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ! [X4] :
( ( ~ v1_xboole_0(X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t45_filter_2) ).
fof(f13644,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( r1_tarski(X1,k20_filter_2(X0,X1,X2))
& r1_tarski(X2,k20_filter_2(X0,X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_filter_2) ).
fof(f13645,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( r1_tarski(X1,k20_filter_2(X0,X1,X2))
& r1_tarski(X2,k20_filter_2(X0,X1,X2)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13644]) ).
fof(f13694,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,[],[f13532]) ).
fof(f13695,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,[],[f13694]) ).
fof(f13696,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,[],[f13533]) ).
fof(f13697,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,[],[f13696]) ).
fof(f13754,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,[],[f13562]) ).
fof(f13755,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,[],[f13754]) ).
fof(f13756,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,[],[f13563]) ).
fof(f13757,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,[],[f13756]) ).
fof(f13831,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,[],[f13602]) ).
fof(f13832,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,[],[f13831]) ).
fof(f13903,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) )
| v1_xboole_0(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v1_xboole_0(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,[],[f13638]) ).
fof(f13904,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) )
| v1_xboole_0(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13903]) ).
fof(f13915,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r1_tarski(X1,k20_filter_2(X0,X1,X2))
| ~ r1_tarski(X2,k20_filter_2(X0,X1,X2)) )
& m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13645]) ).
fof(f13916,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r1_tarski(X1,k20_filter_2(X0,X1,X2))
| ~ r1_tarski(X2,k20_filter_2(X0,X1,X2)) )
& m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f13915]) ).
fof(f13955,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(f13956,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,[],[f13955]) ).
fof(f13989,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(f13990,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13989]) ).
fof(f14033,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_tarski(X1,k5_filter_0(X0,X1,X2))
& r1_tarski(X2,k5_filter_0(X0,X1,X2)) )
| ~ m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8627]) ).
fof(f14034,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_tarski(X1,k5_filter_0(X0,X1,X2))
& r1_tarski(X2,k5_filter_0(X0,X1,X2)) )
| ~ m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14033]) ).
fof(f14055,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(f14056,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,[],[f14055]) ).
fof(f14068,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f14071,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(f14072,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,[],[f14071]) ).
fof(f14073,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(f14074,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14073]) ).
fof(f18248,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,[],[f13695]) ).
fof(f18295,plain,
( ( ~ r1_tarski(sK45,k20_filter_2(sK44,sK45,sK46))
| ~ r1_tarski(sK46,k20_filter_2(sK44,sK45,sK46)) )
& m2_filter_2(sK46,sK44)
& m2_filter_2(sK45,sK44)
& ~ v3_struct_0(sK44)
& v10_lattices(sK44)
& l3_lattices(sK44) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44,sK45,sK46]),skolemize(X0,sK44),skolemize(X1,sK45),skolemize(X2,sK46)],[f13916]) ).
fof(f19739,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,[],[f18248]) ).
fof(f19741,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,[],[f13697]) ).
fof(f19742,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13697]) ).
fof(f19774,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,[],[f13755]) ).
fof(f19775,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,[],[f13757]) ).
fof(f19854,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13832]) ).
fof(f19940,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X4)
| k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13904]) ).
fof(f19952,plain,
l3_lattices(sK44),
inference(cnf_transformation,[],[f18295]) ).
fof(f19953,plain,
v10_lattices(sK44),
inference(cnf_transformation,[],[f18295]) ).
fof(f19954,plain,
~ v3_struct_0(sK44),
inference(cnf_transformation,[],[f18295]) ).
fof(f19955,plain,
m2_filter_2(sK45,sK44),
inference(cnf_transformation,[],[f18295]) ).
fof(f19956,plain,
m2_filter_2(sK46,sK44),
inference(cnf_transformation,[],[f18295]) ).
fof(f19957,plain,
( ~ r1_tarski(sK45,k20_filter_2(sK44,sK45,sK46))
| ~ r1_tarski(sK46,k20_filter_2(sK44,sK45,sK46)) ),
inference(cnf_transformation,[],[f18295]) ).
fof(f20015,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13956]) ).
fof(f20045,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13990]) ).
fof(f20085,plain,
! [X2,X0,X1] :
( r1_tarski(X2,k5_filter_0(X0,X1,X2))
| ~ m1_filter_0(X2,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14034]) ).
fof(f20086,plain,
! [X2,X0,X1] :
( r1_tarski(X1,k5_filter_0(X0,X1,X2))
| ~ m1_filter_0(X2,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14034]) ).
fof(f20108,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f14056]) ).
fof(f20130,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14068]) ).
fof(f20133,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14072]) ).
fof(f20143,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14074]) ).
fof(f28351,definition,
( spl874_36
<=> r1_tarski(sK46,k20_filter_2(sK44,sK45,sK46)) ),
introduced(definition,[new_symbols(definition,[spl874_36])],[avatar_definition]) ).
fof(f28352,plain,
( ~ r1_tarski(sK46,k20_filter_2(sK44,sK45,sK46))
| spl874_36 ),
inference(avatar_component_clause,[],[f28351]) ).
fof(f28354,definition,
( spl874_37
<=> r1_tarski(sK45,k20_filter_2(sK44,sK45,sK46)) ),
introduced(definition,[new_symbols(definition,[spl874_37])],[avatar_definition]) ).
fof(f28356,plain,
( ~ spl874_36
| ~ spl874_37 ),
inference(avatar_split_clause,[],[f19957,f28354,f28351]) ).
fof(f28692,plain,
! [X0] :
( v3_struct_0(sK44)
| k7_filter_2(sK44,X0) = k15_filter_2(sK44,X0)
| ~ l3_lattices(sK44)
| ~ m2_filter_2(X0,sK44) ),
inference(resolution,[],[f19775,f19953]) ).
fof(f28693,plain,
! [X0] :
( k7_filter_2(sK44,X0) = k15_filter_2(sK44,X0)
| ~ l3_lattices(sK44)
| ~ m2_filter_2(X0,sK44) ),
inference(forward_subsumption_resolution,[],[f28692,f19954]) ).
fof(f28694,plain,
! [X0] :
( ~ m2_filter_2(X0,sK44)
| k7_filter_2(sK44,X0) = k15_filter_2(sK44,X0) ),
inference(forward_subsumption_resolution,[],[f28693,f19952]) ).
fof(f28698,plain,
k7_filter_2(sK44,sK45) = k15_filter_2(sK44,sK45),
inference(resolution,[],[f28694,f19955]) ).
fof(f28699,plain,
k7_filter_2(sK44,sK46) = k15_filter_2(sK44,sK46),
inference(resolution,[],[f28694,f19956]) ).
fof(f28700,plain,
! [X0] :
( ~ m2_filter_2(X0,sK44)
| v3_struct_0(sK44)
| m2_lattice4(X0,sK44)
| ~ l3_lattices(sK44) ),
inference(resolution,[],[f19741,f19953]) ).
fof(f28701,plain,
! [X0] :
( ~ m2_filter_2(X0,sK44)
| m2_lattice4(X0,sK44)
| ~ l3_lattices(sK44) ),
inference(forward_subsumption_resolution,[],[f28700,f19954]) ).
fof(f28702,plain,
! [X0] :
( ~ m2_filter_2(X0,sK44)
| m2_lattice4(X0,sK44) ),
inference(forward_subsumption_resolution,[],[f28701,f19952]) ).
fof(f28703,plain,
m2_lattice4(sK45,sK44),
inference(resolution,[],[f28702,f19955]) ).
fof(f28704,plain,
m2_lattice4(sK46,sK44),
inference(resolution,[],[f28702,f19956]) ).
fof(f28707,plain,
( v3_struct_0(sK44)
| v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(sK44) ),
inference(resolution,[],[f20133,f19953]) ).
fof(f28708,plain,
( v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(sK44) ),
inference(forward_subsumption_resolution,[],[f28707,f19954]) ).
fof(f28709,plain,
v10_lattices(k1_lattice2(sK44)),
inference(forward_subsumption_resolution,[],[f28708,f19952]) ).
fof(f28712,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK44))
| v3_struct_0(k1_lattice2(sK44))
| m1_filter_0(X0,k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44)) ),
inference(resolution,[],[f28709,f19739]) ).
fof(f28715,definition,
( spl874_41
<=> l3_lattices(k1_lattice2(sK44)) ),
introduced(definition,[new_symbols(definition,[spl874_41])],[avatar_definition]) ).
fof(f28716,plain,
( ~ l3_lattices(k1_lattice2(sK44))
| spl874_41 ),
inference(avatar_component_clause,[],[f28715]) ).
fof(f28721,definition,
( spl874_43
<=> v3_struct_0(k1_lattice2(sK44)) ),
introduced(definition,[new_symbols(definition,[spl874_43])],[avatar_definition]) ).
fof(f28722,plain,
( v3_struct_0(k1_lattice2(sK44))
| ~ spl874_43 ),
inference(avatar_component_clause,[],[f28721]) ).
fof(f28725,definition,
( spl874_44
<=> ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK44))
| m1_filter_0(X0,k1_lattice2(sK44)) ) ),
introduced(definition,[new_symbols(definition,[spl874_44])],[avatar_definition]) ).
fof(f28726,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK44))
| m1_filter_0(X0,k1_lattice2(sK44)) )
| ~ spl874_44 ),
inference(avatar_component_clause,[],[f28725]) ).
fof(f28727,plain,
( ~ spl874_41
| spl874_43
| spl874_44 ),
inference(avatar_split_clause,[],[f28712,f28725,f28721,f28715]) ).
fof(f28737,plain,
( ~ l3_lattices(sK44)
| spl874_41 ),
inference(resolution,[],[f28716,f20130]) ).
fof(f28739,plain,
( $false
| spl874_41 ),
inference(forward_subsumption_resolution,[],[f28737,f19952]) ).
fof(f28740,plain,
spl874_41,
inference(avatar_contradiction_clause,[],[f28739]) ).
fof(f28742,plain,
( v3_struct_0(sK44)
| ~ l3_lattices(sK44)
| ~ spl874_43 ),
inference(resolution,[],[f28722,f20143]) ).
fof(f28744,plain,
( ~ l3_lattices(sK44)
| ~ spl874_43 ),
inference(forward_subsumption_resolution,[],[f28742,f19954]) ).
fof(f28745,plain,
( $false
| ~ spl874_43 ),
inference(forward_subsumption_resolution,[],[f28744,f19952]) ).
fof(f28746,plain,
~ spl874_43,
inference(avatar_contradiction_clause,[],[f28745]) ).
fof(f28747,plain,
( m1_filter_2(k7_filter_2(sK44,sK45),k1_lattice2(sK44))
| v3_struct_0(sK44)
| ~ v10_lattices(sK44)
| ~ l3_lattices(sK44)
| ~ m2_filter_2(sK45,sK44) ),
inference(superposition,[],[f19774,f28698]) ).
fof(f28748,plain,
( m1_filter_2(k7_filter_2(sK44,sK46),k1_lattice2(sK44))
| v3_struct_0(sK44)
| ~ v10_lattices(sK44)
| ~ l3_lattices(sK44)
| ~ m2_filter_2(sK46,sK44) ),
inference(superposition,[],[f19774,f28699]) ).
fof(f28749,plain,
( m1_filter_2(k7_filter_2(sK44,sK46),k1_lattice2(sK44))
| ~ v10_lattices(sK44)
| ~ l3_lattices(sK44)
| ~ m2_filter_2(sK46,sK44) ),
inference(forward_subsumption_resolution,[],[f28748,f19954]) ).
fof(f28750,plain,
( m1_filter_2(k7_filter_2(sK44,sK45),k1_lattice2(sK44))
| ~ v10_lattices(sK44)
| ~ l3_lattices(sK44)
| ~ m2_filter_2(sK45,sK44) ),
inference(forward_subsumption_resolution,[],[f28747,f19954]) ).
fof(f28751,plain,
( m1_filter_2(k7_filter_2(sK44,sK46),k1_lattice2(sK44))
| ~ l3_lattices(sK44)
| ~ m2_filter_2(sK46,sK44) ),
inference(forward_subsumption_resolution,[],[f28749,f19953]) ).
fof(f28752,plain,
( m1_filter_2(k7_filter_2(sK44,sK45),k1_lattice2(sK44))
| ~ l3_lattices(sK44)
| ~ m2_filter_2(sK45,sK44) ),
inference(forward_subsumption_resolution,[],[f28750,f19953]) ).
fof(f28753,plain,
( m1_filter_2(k7_filter_2(sK44,sK46),k1_lattice2(sK44))
| ~ m2_filter_2(sK46,sK44) ),
inference(forward_subsumption_resolution,[],[f28751,f19952]) ).
fof(f28754,plain,
( m1_filter_2(k7_filter_2(sK44,sK45),k1_lattice2(sK44))
| ~ m2_filter_2(sK45,sK44) ),
inference(forward_subsumption_resolution,[],[f28752,f19952]) ).
fof(f28755,plain,
m1_filter_2(k7_filter_2(sK44,sK46),k1_lattice2(sK44)),
inference(forward_subsumption_resolution,[],[f28753,f19956]) ).
fof(f28756,plain,
m1_filter_2(k7_filter_2(sK44,sK45),k1_lattice2(sK44)),
inference(forward_subsumption_resolution,[],[f28754,f19955]) ).
fof(f28760,plain,
( m1_filter_0(k7_filter_2(sK44,sK45),k1_lattice2(sK44))
| ~ spl874_44 ),
inference(resolution,[],[f28726,f28756]) ).
fof(f28761,plain,
( m1_filter_0(k7_filter_2(sK44,sK46),k1_lattice2(sK44))
| ~ spl874_44 ),
inference(resolution,[],[f28726,f28755]) ).
fof(f28777,plain,
( v3_struct_0(sK44)
| u1_struct_0(sK44) = k1_filter_0(sK44)
| ~ l3_lattices(sK44) ),
inference(resolution,[],[f20045,f19953]) ).
fof(f28783,plain,
( u1_struct_0(sK44) = k1_filter_0(sK44)
| ~ l3_lattices(sK44) ),
inference(forward_subsumption_resolution,[],[f28777,f19954]) ).
fof(f28784,plain,
u1_struct_0(sK44) = k1_filter_0(sK44),
inference(forward_subsumption_resolution,[],[f28783,f19952]) ).
fof(f28785,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| k7_filter_2(sK44,X0) = X0
| v3_struct_0(sK44)
| ~ v10_lattices(sK44)
| ~ l3_lattices(sK44) ),
inference(superposition,[],[f19854,f28784]) ).
fof(f28790,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| k7_filter_2(sK44,X0) = X0
| ~ v10_lattices(sK44)
| ~ l3_lattices(sK44) ),
inference(forward_subsumption_resolution,[],[f28785,f19954]) ).
fof(f28793,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| k7_filter_2(sK44,X0) = X0
| ~ l3_lattices(sK44) ),
inference(forward_subsumption_resolution,[],[f28790,f19953]) ).
fof(f28796,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| k7_filter_2(sK44,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f28793,f19952]) ).
fof(f28828,plain,
( v3_struct_0(sK44)
| u1_struct_0(sK44) = u1_struct_0(k1_lattice2(sK44)) ),
inference(resolution,[],[f20108,f19952]) ).
fof(f28830,plain,
u1_struct_0(sK44) = u1_struct_0(k1_lattice2(sK44)),
inference(forward_subsumption_resolution,[],[f28828,f19954]) ).
fof(f28831,plain,
u1_struct_0(k1_lattice2(sK44)) = k1_filter_0(sK44),
inference(forward_demodulation,[],[f28830,f28784]) ).
fof(f28832,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X0)
| k20_filter_2(sK44,X1,X2) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X1),k7_filter_2(sK44,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK44)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK44)))
| v3_struct_0(sK44)
| ~ v10_lattices(sK44)
| ~ l3_lattices(sK44) ),
inference(superposition,[],[f19940,f28831]) ).
fof(f28839,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X0)
| k20_filter_2(sK44,X1,X2) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X1),k7_filter_2(sK44,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK44)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK44)))
| ~ v10_lattices(sK44)
| ~ l3_lattices(sK44) ),
inference(forward_subsumption_resolution,[],[f28832,f19954]) ).
fof(f28855,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X0)
| k20_filter_2(sK44,X1,X2) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X1),k7_filter_2(sK44,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK44)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK44)))
| ~ l3_lattices(sK44) ),
inference(forward_subsumption_resolution,[],[f28839,f19953]) ).
fof(f28856,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X0)
| k20_filter_2(sK44,X1,X2) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X1),k7_filter_2(sK44,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK44)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK44))) ),
inference(forward_subsumption_resolution,[],[f28855,f19952]) ).
fof(f28857,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_filter_0(sK44)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X0)
| k20_filter_2(sK44,X1,X2) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X1),k7_filter_2(sK44,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK44))) ),
inference(forward_demodulation,[],[f28856,f28784]) ).
fof(f28858,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_filter_0(sK44)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_filter_0(sK44)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X0)
| k20_filter_2(sK44,X1,X2) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X1),k7_filter_2(sK44,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X2)
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f28857,f28784]) ).
fof(f28860,definition,
( spl874_59
<=> ! [X3] :
( v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_filter_0(sK44))) ) ),
introduced(definition,[new_symbols(definition,[spl874_59])],[avatar_definition]) ).
fof(f28861,plain,
( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X3) )
| ~ spl874_59 ),
inference(avatar_component_clause,[],[f28860]) ).
fof(f28863,definition,
( spl874_60
<=> ! [X2,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| k20_filter_2(sK44,X1,X2) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X1),k7_filter_2(sK44,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_filter_0(sK44))) ) ),
introduced(definition,[new_symbols(definition,[spl874_60])],[avatar_definition]) ).
fof(f28864,plain,
( ! [X2,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| k20_filter_2(sK44,X1,X2) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X1),k7_filter_2(sK44,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_filter_0(sK44))) )
| ~ spl874_60 ),
inference(avatar_component_clause,[],[f28863]) ).
fof(f28865,plain,
( spl874_59
| spl874_59
| spl874_60 ),
inference(avatar_split_clause,[],[f28858,f28863,f28860,f28860]) ).
fof(f28967,plain,
! [X0] :
( ~ m2_lattice4(X0,sK44)
| v3_struct_0(sK44)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK44)))
| ~ l3_lattices(sK44) ),
inference(resolution,[],[f20015,f19953]) ).
fof(f28970,plain,
! [X0] :
( ~ m2_lattice4(X0,sK44)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK44)))
| ~ l3_lattices(sK44) ),
inference(forward_subsumption_resolution,[],[f28967,f19954]) ).
fof(f28972,plain,
! [X0] :
( ~ m2_lattice4(X0,sK44)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK44))) ),
inference(forward_subsumption_resolution,[],[f28970,f19952]) ).
fof(f28977,plain,
! [X0] :
( ~ m2_lattice4(X0,sK44)
| m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44))) ),
inference(forward_demodulation,[],[f28972,f28784]) ).
fof(f28978,plain,
m1_subset_1(sK45,k1_zfmisc_1(k1_filter_0(sK44))),
inference(resolution,[],[f28977,f28703]) ).
fof(f28979,plain,
m1_subset_1(sK46,k1_zfmisc_1(k1_filter_0(sK44))),
inference(resolution,[],[f28977,f28704]) ).
fof(f28983,plain,
( v1_xboole_0(sK45)
| ~ spl874_59 ),
inference(resolution,[],[f28978,f28861]) ).
fof(f28984,plain,
sK45 = k7_filter_2(sK44,sK45),
inference(resolution,[],[f28978,f28796]) ).
fof(f28989,plain,
( $false
| ~ spl874_59 ),
inference(unit_resulting_resolution,[],[f19742,f19952,f19953,f19954,f19955,f28983]) ).
fof(f28991,plain,
~ spl874_59,
inference(avatar_contradiction_clause,[],[f28989]) ).
fof(f28998,definition,
( spl874_68
<=> v1_xboole_0(sK45) ),
introduced(definition,[new_symbols(definition,[spl874_68])],[avatar_definition]) ).
fof(f28999,plain,
( v1_xboole_0(sK45)
| ~ spl874_68 ),
inference(avatar_component_clause,[],[f28998]) ).
fof(f29010,plain,
( $false
| ~ spl874_68 ),
inference(unit_resulting_resolution,[],[f19742,f19952,f19953,f19954,f19955,f28999]) ).
fof(f29012,plain,
~ spl874_68,
inference(avatar_contradiction_clause,[],[f29010]) ).
fof(f29014,plain,
( m1_filter_0(sK45,k1_lattice2(sK44))
| ~ spl874_44 ),
inference(superposition,[],[f28760,f28984]) ).
fof(f29039,plain,
( ! [X0] :
( v1_xboole_0(X0)
| v1_xboole_0(sK46)
| k20_filter_2(sK44,X0,sK46) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X0),k7_filter_2(sK44,sK46))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44))) )
| ~ spl874_60 ),
inference(resolution,[],[f28979,f28864]) ).
fof(f29042,plain,
sK46 = k7_filter_2(sK44,sK46),
inference(resolution,[],[f28979,f28796]) ).
fof(f29048,definition,
( spl874_73
<=> v1_xboole_0(sK46) ),
introduced(definition,[new_symbols(definition,[spl874_73])],[avatar_definition]) ).
fof(f29049,plain,
( v1_xboole_0(sK46)
| ~ spl874_73 ),
inference(avatar_component_clause,[],[f29048]) ).
fof(f29052,plain,
( ! [X0] :
( k20_filter_2(sK44,X0,sK46) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X0),sK46)
| v1_xboole_0(X0)
| v1_xboole_0(sK46)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44))) )
| ~ spl874_60 ),
inference(forward_demodulation,[],[f29039,f29042]) ).
fof(f29055,definition,
( spl874_74
<=> ! [X0] :
( k20_filter_2(sK44,X0,sK46) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X0),sK46)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl874_74])],[avatar_definition]) ).
fof(f29056,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK44)))
| k20_filter_2(sK44,X0,sK46) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,X0),sK46)
| v1_xboole_0(X0) )
| ~ spl874_74 ),
inference(avatar_component_clause,[],[f29055]) ).
fof(f29057,plain,
( spl874_73
| spl874_74
| ~ spl874_60 ),
inference(avatar_split_clause,[],[f29052,f28863,f29055,f29048]) ).
fof(f29064,plain,
( $false
| ~ spl874_73 ),
inference(unit_resulting_resolution,[],[f19742,f19952,f19953,f19954,f19956,f29049]) ).
fof(f29066,plain,
~ spl874_73,
inference(avatar_contradiction_clause,[],[f29064]) ).
fof(f29085,plain,
( m1_filter_0(sK46,k1_lattice2(sK44))
| ~ spl874_44 ),
inference(superposition,[],[f28761,f29042]) ).
fof(f29093,plain,
( k20_filter_2(sK44,sK45,sK46) = k5_filter_0(k1_lattice2(sK44),k7_filter_2(sK44,sK45),sK46)
| v1_xboole_0(sK45)
| ~ spl874_74 ),
inference(resolution,[],[f29056,f28978]) ).
fof(f29096,plain,
( k20_filter_2(sK44,sK45,sK46) = k5_filter_0(k1_lattice2(sK44),sK45,sK46)
| v1_xboole_0(sK45)
| ~ spl874_74 ),
inference(forward_demodulation,[],[f29093,f28984]) ).
fof(f29102,definition,
( spl874_80
<=> k20_filter_2(sK44,sK45,sK46) = k5_filter_0(k1_lattice2(sK44),sK45,sK46) ),
introduced(definition,[new_symbols(definition,[spl874_80])],[avatar_definition]) ).
fof(f29103,plain,
( k20_filter_2(sK44,sK45,sK46) = k5_filter_0(k1_lattice2(sK44),sK45,sK46)
| ~ spl874_80 ),
inference(avatar_component_clause,[],[f29102]) ).
fof(f29104,plain,
( spl874_68
| spl874_80
| ~ spl874_74 ),
inference(avatar_split_clause,[],[f29096,f29055,f29102,f28998]) ).
fof(f29105,plain,
( r1_tarski(sK46,k20_filter_2(sK44,sK45,sK46))
| ~ m1_filter_0(sK46,k1_lattice2(sK44))
| ~ m1_filter_0(sK45,k1_lattice2(sK44))
| v3_struct_0(k1_lattice2(sK44))
| ~ v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| ~ spl874_80 ),
inference(superposition,[],[f20085,f29103]) ).
fof(f29106,plain,
( r1_tarski(sK45,k20_filter_2(sK44,sK45,sK46))
| ~ m1_filter_0(sK46,k1_lattice2(sK44))
| ~ m1_filter_0(sK45,k1_lattice2(sK44))
| v3_struct_0(k1_lattice2(sK44))
| ~ v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| ~ spl874_80 ),
inference(superposition,[],[f20086,f29103]) ).
fof(f29107,plain,
( r1_tarski(sK45,k20_filter_2(sK44,sK45,sK46))
| ~ m1_filter_0(sK45,k1_lattice2(sK44))
| v3_struct_0(k1_lattice2(sK44))
| ~ v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| ~ spl874_44
| ~ spl874_80 ),
inference(forward_subsumption_resolution,[],[f29106,f29085]) ).
fof(f29108,plain,
( ~ m1_filter_0(sK46,k1_lattice2(sK44))
| ~ m1_filter_0(sK45,k1_lattice2(sK44))
| v3_struct_0(k1_lattice2(sK44))
| ~ v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| spl874_36
| ~ spl874_80 ),
inference(forward_subsumption_resolution,[],[f29105,f28352]) ).
fof(f29109,plain,
( r1_tarski(sK45,k20_filter_2(sK44,sK45,sK46))
| v3_struct_0(k1_lattice2(sK44))
| ~ v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| ~ spl874_44
| ~ spl874_80 ),
inference(forward_subsumption_resolution,[],[f29107,f29014]) ).
fof(f29110,plain,
( ~ m1_filter_0(sK45,k1_lattice2(sK44))
| v3_struct_0(k1_lattice2(sK44))
| ~ v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| spl874_36
| ~ spl874_44
| ~ spl874_80 ),
inference(forward_subsumption_resolution,[],[f29108,f29085]) ).
fof(f29111,plain,
( r1_tarski(sK45,k20_filter_2(sK44,sK45,sK46))
| v3_struct_0(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| ~ spl874_44
| ~ spl874_80 ),
inference(forward_subsumption_resolution,[],[f29109,f28709]) ).
fof(f29112,plain,
( v3_struct_0(k1_lattice2(sK44))
| ~ v10_lattices(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| spl874_36
| ~ spl874_44
| ~ spl874_80 ),
inference(forward_subsumption_resolution,[],[f29110,f29014]) ).
fof(f29114,plain,
( ~ spl874_41
| spl874_43
| spl874_37
| ~ spl874_44
| ~ spl874_80 ),
inference(avatar_split_clause,[],[f29111,f29102,f28725,f28354,f28721,f28715]) ).
fof(f29115,plain,
( v3_struct_0(k1_lattice2(sK44))
| ~ l3_lattices(k1_lattice2(sK44))
| spl874_36
| ~ spl874_44
| ~ spl874_80 ),
inference(forward_subsumption_resolution,[],[f29112,f28709]) ).
fof(f29116,plain,
( ~ spl874_41
| spl874_43
| spl874_36
| ~ spl874_44
| ~ spl874_80 ),
inference(avatar_split_clause,[],[f29115,f29102,f28725,f28351,f28721,f28715]) ).
cnf(s14,plain,
( ~ spl874_36
| ~ spl874_37 ),
inference(sat_conversion,[],[f28356]) ).
cnf(s36,plain,
( ~ spl874_41
| spl874_43
| spl874_44 ),
inference(sat_conversion,[],[f28727]) ).
cnf(s40,plain,
spl874_41,
inference(sat_conversion,[],[f28740]) ).
cnf(s42,plain,
~ spl874_43,
inference(sat_conversion,[],[f28746]) ).
cnf(s51,plain,
( spl874_59
| spl874_59
| spl874_60 ),
inference(sat_conversion,[],[f28865]) ).
cnf(s52,plain,
( spl874_59
| spl874_60 ),
inference(rat,[],[s51]) ).
cnf(s62,plain,
~ spl874_59,
inference(sat_conversion,[],[f28991]) ).
cnf(s65,plain,
~ spl874_68,
inference(sat_conversion,[],[f29012]) ).
cnf(s70,plain,
( ~ spl874_60
| spl874_73
| spl874_74 ),
inference(sat_conversion,[],[f29057]) ).
cnf(s72,plain,
~ spl874_73,
inference(sat_conversion,[],[f29066]) ).
cnf(s77,plain,
( spl874_68
| ~ spl874_74
| spl874_80 ),
inference(sat_conversion,[],[f29104]) ).
cnf(s78,plain,
( spl874_37
| ~ spl874_41
| spl874_43
| ~ spl874_44
| ~ spl874_80 ),
inference(sat_conversion,[],[f29114]) ).
cnf(s79,plain,
( spl874_36
| ~ spl874_41
| spl874_43
| ~ spl874_44
| ~ spl874_80 ),
inference(sat_conversion,[],[f29116]) ).
cnf(s81,plain,
( ~ spl874_60
| spl874_74 ),
inference(rat,[],[s70,s72]) ).
cnf(s85,plain,
spl874_60,
inference(rat,[],[s52,s62]) ).
cnf(s86,plain,
spl874_74,
inference(rat,[],[s81,s85]) ).
cnf(s88,plain,
spl874_80,
inference(rat,[],[s77,s65,s86]) ).
cnf(s106,plain,
spl874_44,
inference(rat,[],[s36,s42,s40]) ).
cnf(s110,plain,
spl874_36,
inference(rat,[],[s79,s88,s40,s42,s106]) ).
cnf(s111,plain,
spl874_37,
inference(rat,[],[s78,s88,s40,s42,s106]) ).
cnf(s115,plain,
$false,
inference(rat,[],[s14,s111,s110]) ).
fof(f29117,plain,
$false,
inference(avatar_sat_refutation,[],[s115]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT317+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 14:33:08 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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
% 15.57/3.76 % (287492)Detected formulas, will run a generic FOF schedule.
% 15.57/3.76 % (287497)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=4196781406:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 15.57/3.76 % (287499)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=3593678853:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 15.57/3.76 % (287500)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1100144392:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 15.57/3.76 % (287503)dis-21_1_sil=8000:lcm=predicate:random_seed=2978893281: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.57/3.76 % (287501)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2176715932:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 15.57/3.76 % (287498)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=1122303738:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 15.57/3.76 % (287502)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3277177132:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 15.57/3.76 % (287500)Refutation not found, incomplete strategy
% 15.57/3.76 % (287500)------------------------------
% 15.57/3.76 % (287500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/3.76 % (287500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/3.76 % (287500)CaDiCaL version: 2.1.3
% 15.57/3.76 % (287500)Termination reason: Refutation not found, incomplete strategy
% 15.57/3.76 % (287500)Time elapsed: 0.068 s
% 15.57/3.76 % (287500)Peak memory usage: 107 MB
% 15.57/3.76 % (287500)Instructions burned: 85 (million)
% 15.57/3.76 % (287502)Instruction limit reached!
% 15.57/3.76 % (287502)------------------------------
% 15.57/3.76 % (287502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/3.76 % (287502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/3.76 % (287502)CaDiCaL version: 2.1.3
% 15.57/3.76 % (287502)Termination reason: Instruction limit
% 15.57/3.76 % (287502)Termination phase: Property scanning
% 15.57/3.76 % (287502)Time elapsed: 0.060 s
% 15.57/3.76 % (287502)Peak memory usage: 102 MB
% 15.57/3.76 % (287502)Instructions burned: 141 (million)
% 15.57/3.76 % (287501)Instruction limit reached!
% 15.57/3.76 % (287501)------------------------------
% 15.57/3.76 % (287501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/3.76 % (287501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/3.76 % (287501)CaDiCaL version: 2.1.3
% 15.57/3.76 % (287501)Termination reason: Instruction limit
% 15.57/3.76 % (287501)Termination phase: Property scanning
% 15.57/3.76 % (287501)Time elapsed: 0.091 s
% 15.57/3.76 % (287501)Peak memory usage: 105 MB
% 15.57/3.76 % (287501)Instructions burned: 119 (million)
% 15.57/3.76 % (287503)Instruction limit reached!
% 15.57/3.76 % (287503)------------------------------
% 15.57/3.76 % (287503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/3.76 % (287503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/3.76 % (287503)CaDiCaL version: 2.1.3
% 15.57/3.76 % (287503)Termination reason: Instruction limit
% 15.57/3.76 % (287503)Termination phase: Preprocessing 1
% 15.57/3.76 % (287503)Time elapsed: 0.093 s
% 15.57/3.76 % (287503)Peak memory usage: 103 MB
% 15.57/3.76 % (287503)Instructions burned: 129 (million)
% 15.57/3.76 % (287511)lrs+10_1_sil=8000:sp=occurrence:random_seed=1284401334:i=285:sd=3:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/285Mi)
% 15.57/3.76 % (287513)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2129096615:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 15.57/3.76 % (287512)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3829137946:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 15.57/3.76 % (287500)------------------------------
% 15.57/3.76 % (287500)------------------------------
% 15.57/3.76 % (287512)Instruction limit reached!
% 15.57/3.76 % (287512)------------------------------
% 15.57/3.76 % (287512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/3.76 % (287512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287512)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287512)Termination reason: Instruction limit
% 18.54/4.46 % (287512)Termination phase: Property scanning
% 18.54/4.46 % (287512)Time elapsed: 0.067 s
% 18.54/4.46 % (287512)Peak memory usage: 102 MB
% 18.54/4.46 % (287512)Instructions burned: 158 (million)
% 18.54/4.46 % (287511)Instruction limit reached!
% 18.54/4.46 % (287511)------------------------------
% 18.54/4.46 % (287511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287511)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287511)Termination reason: Instruction limit
% 18.54/4.46 % (287511)Termination phase: Saturation
% 18.54/4.46 % (287511)Time elapsed: 0.200 s
% 18.54/4.46 % (287511)Peak memory usage: 109 MB
% 18.54/4.46 % (287511)Instructions burned: 287 (million)
% 18.54/4.46 % (287518)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2744646022:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 18.54/4.46 % (287517)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=1575994188:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 18.54/4.46 % (287513)Instruction limit reached!
% 18.54/4.46 % (287513)------------------------------
% 18.54/4.46 % (287513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287513)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287513)Termination reason: Instruction limit
% 18.54/4.46 % (287513)Termination phase: Saturation
% 18.54/4.46 % (287513)Time elapsed: 0.223 s
% 18.54/4.46 % (287513)Peak memory usage: 108 MB
% 18.54/4.46 % (287513)Instructions burned: 326 (million)
% 18.54/4.46 % (287519)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2947365460:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 18.54/4.46 % (287517)Instruction limit reached!
% 18.54/4.46 % (287517)------------------------------
% 18.54/4.46 % (287517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287517)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287517)Termination reason: Instruction limit
% 18.54/4.46 % (287517)Termination phase: SInE selection
% 18.54/4.46 % (287517)Time elapsed: 0.126 s
% 18.54/4.46 % (287517)Peak memory usage: 103 MB
% 18.54/4.46 % (287517)Instructions burned: 249 (million)
% 18.54/4.46 % (287522)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4201767886:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 18.54/4.46 % (287518)Instruction limit reached!
% 18.54/4.46 % (287518)------------------------------
% 18.54/4.46 % (287518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287518)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287518)Termination reason: Instruction limit
% 18.54/4.46 % (287518)Termination phase: Saturation
% 18.54/4.46 % (287518)Time elapsed: 0.196 s
% 18.54/4.46 % (287518)Peak memory usage: 110 MB
% 18.54/4.46 % (287518)Instructions burned: 295 (million)
% 18.54/4.46 % (287522)Instruction limit reached!
% 18.54/4.46 % (287522)------------------------------
% 18.54/4.46 % (287522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287522)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287522)Termination reason: Instruction limit
% 18.54/4.46 % (287522)Termination phase: Preprocessing 3
% 18.54/4.46 % (287522)Time elapsed: 0.096 s
% 18.54/4.46 % (287522)Peak memory usage: 105 MB
% 18.54/4.46 % (287522)Instructions burned: 114 (million)
% 18.54/4.46 % (287524)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2091898782:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 18.54/4.46 % (287526)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2513157334:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 18.54/4.46 % (287524)Instruction limit reached!
% 18.54/4.46 % (287524)------------------------------
% 18.54/4.46 % (287524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287524)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287524)Termination reason: Instruction limit
% 18.54/4.46 % (287524)Termination phase: Preprocessing 2
% 18.54/4.46 % (287524)Time elapsed: 0.104 s
% 18.54/4.46 % (287524)Peak memory usage: 106 MB
% 18.54/4.46 % (287524)Instructions burned: 128 (million)
% 18.54/4.46 % (287526)Instruction limit reached!
% 18.54/4.46 % (287526)------------------------------
% 18.54/4.46 % (287526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287526)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287526)Termination reason: Instruction limit
% 18.54/4.46 % (287526)Termination phase: Property scanning
% 18.54/4.46 % (287526)Time elapsed: 0.049 s
% 18.54/4.46 % (287526)Peak memory usage: 102 MB
% 18.54/4.46 % (287526)Instructions burned: 115 (million)
% 18.54/4.46 % (287527)lrs+10_1_sil=8000:sp=occurrence:random_seed=3891234361:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 18.54/4.46 % (287530)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=206572680:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 18.54/4.46 % (287531)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1470082505:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 18.54/4.46 % (287530)Instruction limit reached!
% 18.54/4.46 % (287530)------------------------------
% 18.54/4.46 % (287530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287530)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287530)Termination reason: Instruction limit
% 18.54/4.46 % (287530)Termination phase: Saturation
% 18.54/4.46 % (287530)Time elapsed: 0.287 s
% 18.54/4.46 % (287530)Peak memory usage: 109 MB
% 18.54/4.46 % (287530)Instructions burned: 438 (million)
% 18.54/4.46 % (287535)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=930894437:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 18.54/4.46 % (287527)Instruction limit reached!
% 18.54/4.46 % (287527)------------------------------
% 18.54/4.46 % (287527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287527)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287527)Termination reason: Instruction limit
% 18.54/4.46 % (287527)Termination phase: Saturation
% 18.54/4.46 % (287527)Time elapsed: 0.594 s
% 18.54/4.46 % (287527)Peak memory usage: 121 MB
% 18.54/4.46 % (287527)Instructions burned: 908 (million)
% 18.54/4.46 % (287535)Instruction limit reached!
% 18.54/4.46 % (287535)------------------------------
% 18.54/4.46 % (287535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287535)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287535)Termination reason: Instruction limit
% 18.54/4.46 % (287535)Termination phase: Property scanning
% 18.54/4.46 % (287535)Time elapsed: 0.102 s
% 18.54/4.46 % (287535)Peak memory usage: 106 MB
% 18.54/4.46 % (287535)Instructions burned: 134 (million)
% 18.54/4.46 % (287537)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2450764758:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 18.54/4.46 % (287538)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2288521659:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 18.54/4.46 % (287519)Instruction limit reached!
% 18.54/4.46 % (287519)------------------------------
% 18.54/4.46 % (287519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287519)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287519)Termination reason: Instruction limit
% 18.54/4.46 % (287519)Termination phase: Saturation
% 18.54/4.46 % (287519)Time elapsed: 1.435 s
% 18.54/4.46 % (287519)Peak memory usage: 239 MB
% 18.54/4.46 % (287519)Instructions burned: 2350 (million)
% 18.54/4.46 % (287537)Instruction limit reached!
% 18.54/4.46 % (287537)------------------------------
% 18.54/4.46 % (287537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287537)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287537)Termination reason: Instruction limit
% 18.54/4.46 % (287537)Termination phase: Property scanning
% 18.54/4.46 % (287537)Time elapsed: 0.390 s
% 18.54/4.46 % (287537)Peak memory usage: 123 MB
% 18.54/4.46 % (287537)Instructions burned: 594 (million)
% 18.54/4.46 % (287541)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=649617175:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/125Mi)
% 18.54/4.46 % (287542)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4105385734:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 18.54/4.46 % (287541)Instruction limit reached!
% 18.54/4.46 % (287541)------------------------------
% 18.54/4.46 % (287541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287541)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287541)Termination reason: Instruction limit
% 18.54/4.46 % (287541)Termination phase: Property scanning
% 18.54/4.46 % (287541)Time elapsed: 0.054 s
% 18.54/4.46 % (287541)Peak memory usage: 102 MB
% 18.54/4.46 % (287541)Instructions burned: 125 (million)
% 18.54/4.46 % (287542)Instruction limit reached!
% 18.54/4.46 % (287542)------------------------------
% 18.54/4.46 % (287542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287542)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287542)Termination reason: Instruction limit
% 18.54/4.46 % (287542)Termination phase: Property scanning
% 18.54/4.46 % (287542)Time elapsed: 0.057 s
% 18.54/4.46 % (287542)Peak memory usage: 102 MB
% 18.54/4.46 % (287542)Instructions burned: 134 (million)
% 18.54/4.46 % (287545)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1448191288:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 18.54/4.46 % (287498)First to succeed.
% 18.54/4.46 % (287498)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-287492"
% 18.54/4.46 % (287546)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4083471581:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2968 on theBenchmark for (2968ds/431Mi)
% 18.54/4.46 % (287545)Refutation not found, incomplete strategy
% 18.54/4.46 % (287545)------------------------------
% 18.54/4.46 % (287545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/4.46 % (287545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/4.46 % (287545)CaDiCaL version: 2.1.3
% 18.54/4.46 % (287545)Termination reason: Refutation not found, incomplete strategy
% 18.54/4.46 % (287545)Time elapsed: 0.073 s
% 18.54/4.46 % (287545)Peak memory usage: 107 MB
% 18.54/4.46 % (287545)Instructions burned: 86 (million)
% 18.54/4.46 % (287498)Refutation found. Thanks to Tanya!
% 18.54/4.46 % SZS status Theorem for theBenchmark
% 18.54/4.46 % SZS output start Proof for theBenchmark
% See solution above
% 21.90/4.67 % (287498)------------------------------
% 21.90/4.67 % (287498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.90/4.67 % (287498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/4.67 % (287498)CaDiCaL version: 2.1.3
% 21.90/4.67 % (287498)Termination reason: Refutation
% 21.90/4.67 % (287498)Time elapsed: 2.450 s
% 21.90/4.67 % (287498)Peak memory usage: 215 MB
% 21.90/4.67 % (287498)Instructions burned: 4068 (million)
% 21.90/4.67 % (287498)------------------------------
% 21.90/4.67 % (287498)------------------------------
% 21.90/4.67 % (287492)Success in time 3.617 s
% 21.90/4.67 % Vampire exiting
%------------------------------------------------------------------------------