%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT331+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:01 AM UTC 2026
% Result : Theorem 42.13s 8.79s
% Output : Refutation 43.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 16
% Syntax : Number of formulae : 210 ( 52 unt; 7 def)
% Number of atoms : 700 ( 136 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 803 ( 313 ~; 338 |; 122 &)
% ( 9 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 21 ( 19 usr; 7 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-3 aty)
% Number of variables : 102 ( 0 sgn 94 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21499,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_filter_0(X1,X0) )
=> ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v3_lattices(k8_filter_0(X0,X1))
& v4_lattices(k8_filter_0(X0,X1))
& v5_lattices(k8_filter_0(X0,X1))
& v6_lattices(k8_filter_0(X0,X1))
& v7_lattices(k8_filter_0(X0,X1))
& v8_lattices(k8_filter_0(X0,X1))
& v9_lattices(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_filter_0) ).
fof(f21569,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( u1_struct_0(k8_filter_0(X0,X1)) = X1
& u2_lattices(k8_filter_0(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k8_filter_0(X0,X1)) = k1_realset1(u1_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_filter_0) ).
fof(f21611,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_filter_0(X1,X0) )
=> ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_filter_0) ).
fof(f22780,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(f22781,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_lattice2) ).
fof(f34606,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(f34656,axiom,
! [X0] :
( l3_lattices(X0)
=> ! [X1] :
( l3_lattices(X1)
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> k1_lattice2(X0) = k1_lattice2(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_filter_2) ).
fof(f34657,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(f34738,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_filter_2(X2,X0)
=> ! [X3] :
( m1_filter_2(X3,X1)
=> ( ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& X2 = X3 )
=> k8_filter_0(X0,X2) = k8_filter_0(X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t68_filter_2) ).
fof(f34739,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_filter_2(X2,X0)
=> ! [X3] :
( m1_filter_2(X3,X1)
=> ( ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& X2 = X3 )
=> k8_filter_0(X0,X2) = k8_filter_0(X1,X3) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34738]) ).
fof(f35032,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k8_filter_0(X0,X2) != k8_filter_0(X1,X3)
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& X2 = X3
& m1_filter_2(X3,X1) )
& m1_filter_2(X2,X0) )
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34739]) ).
fof(f35033,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k8_filter_0(X0,X2) != k8_filter_0(X1,X3)
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& X2 = X3
& m1_filter_2(X3,X1) )
& m1_filter_2(X2,X0) )
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f35032]) ).
fof(f35044,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,[],[f34606]) ).
fof(f35045,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,[],[f35044]) ).
fof(f35060,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,[],[f34657]) ).
fof(f35061,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,[],[f35060]) ).
fof(f35062,plain,
! [X0] :
( ! [X1] :
( k1_lattice2(X0) = k1_lattice2(X1)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34656]) ).
fof(f35063,plain,
! [X0] :
( ! [X1] :
( k1_lattice2(X0) = k1_lattice2(X1)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1) )
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35062]) ).
fof(f35109,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,[],[f22780]) ).
fof(f35110,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,[],[f35109]) ).
fof(f35149,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(ennf_transformation,[],[f21611]) ).
fof(f35150,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(flattening,[],[f35149]) ).
fof(f35175,plain,
! [X0] :
( ! [X1] :
( ( u1_struct_0(k8_filter_0(X0,X1)) = X1
& u2_lattices(k8_filter_0(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k8_filter_0(X0,X1)) = k1_realset1(u1_lattices(X0),X1) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21569]) ).
fof(f35176,plain,
! [X0] :
( ! [X1] :
( ( u1_struct_0(k8_filter_0(X0,X1)) = X1
& u2_lattices(k8_filter_0(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k8_filter_0(X0,X1)) = k1_realset1(u1_lattices(X0),X1) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35175]) ).
fof(f35181,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v3_lattices(k8_filter_0(X0,X1))
& v4_lattices(k8_filter_0(X0,X1))
& v5_lattices(k8_filter_0(X0,X1))
& v6_lattices(k8_filter_0(X0,X1))
& v7_lattices(k8_filter_0(X0,X1))
& v8_lattices(k8_filter_0(X0,X1))
& v9_lattices(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(ennf_transformation,[],[f21499]) ).
fof(f35182,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v3_lattices(k8_filter_0(X0,X1))
& v4_lattices(k8_filter_0(X0,X1))
& v5_lattices(k8_filter_0(X0,X1))
& v6_lattices(k8_filter_0(X0,X1))
& v7_lattices(k8_filter_0(X0,X1))
& v8_lattices(k8_filter_0(X0,X1))
& v9_lattices(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(flattening,[],[f35181]) ).
fof(f35234,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22781]) ).
fof(f35235,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35234]) ).
fof(f40598,definition,
! [X1,X0] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v3_lattices(k8_filter_0(X0,X1))
& v4_lattices(k8_filter_0(X0,X1))
& v5_lattices(k8_filter_0(X0,X1))
& v6_lattices(k8_filter_0(X0,X1))
& v7_lattices(k8_filter_0(X0,X1))
& v8_lattices(k8_filter_0(X0,X1))
& v9_lattices(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1)) )
| ~ sP2(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f40599,plain,
! [X0,X1] :
( sP2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(definition_folding,[],[f35182,f40598]) ).
fof(f40897,plain,
( k8_filter_0(sK207,sK209) != k8_filter_0(sK208,sK210)
& g3_lattices(u1_struct_0(sK207),u2_lattices(sK207),u1_lattices(sK207)) = g3_lattices(u1_struct_0(sK208),u2_lattices(sK208),u1_lattices(sK208))
& sK209 = sK210
& m1_filter_2(sK210,sK208)
& m1_filter_2(sK209,sK207)
& ~ v3_struct_0(sK208)
& v10_lattices(sK208)
& l3_lattices(sK208)
& ~ v3_struct_0(sK207)
& v10_lattices(sK207)
& l3_lattices(sK207) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK207,sK208,sK209,sK210]),skolemize(X0,sK207),skolemize(X1,sK208),skolemize(X2,sK209),skolemize(X3,sK210)],[f35033]) ).
fof(f40900,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,[],[f35045]) ).
fof(f40910,plain,
! [X1,X0] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v3_lattices(k8_filter_0(X0,X1))
& v4_lattices(k8_filter_0(X0,X1))
& v5_lattices(k8_filter_0(X0,X1))
& v6_lattices(k8_filter_0(X0,X1))
& v7_lattices(k8_filter_0(X0,X1))
& v8_lattices(k8_filter_0(X0,X1))
& v9_lattices(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1)) )
| ~ sP2(X1,X0) ),
inference(nnf_transformation,[],[f40598]) ).
fof(f40911,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X1,X0))
& v3_lattices(k8_filter_0(X1,X0))
& v4_lattices(k8_filter_0(X1,X0))
& v5_lattices(k8_filter_0(X1,X0))
& v6_lattices(k8_filter_0(X1,X0))
& v7_lattices(k8_filter_0(X1,X0))
& v8_lattices(k8_filter_0(X1,X0))
& v9_lattices(k8_filter_0(X1,X0))
& v10_lattices(k8_filter_0(X1,X0)) )
| ~ sP2(X0,X1) ),
inference(rectify,[],[f40910]) ).
fof(f42882,plain,
l3_lattices(sK207),
inference(cnf_transformation,[],[f40897]) ).
fof(f42883,plain,
v10_lattices(sK207),
inference(cnf_transformation,[],[f40897]) ).
fof(f42884,plain,
~ v3_struct_0(sK207),
inference(cnf_transformation,[],[f40897]) ).
fof(f42885,plain,
l3_lattices(sK208),
inference(cnf_transformation,[],[f40897]) ).
fof(f42886,plain,
v10_lattices(sK208),
inference(cnf_transformation,[],[f40897]) ).
fof(f42887,plain,
~ v3_struct_0(sK208),
inference(cnf_transformation,[],[f40897]) ).
fof(f42888,plain,
m1_filter_2(sK209,sK207),
inference(cnf_transformation,[],[f40897]) ).
fof(f42889,plain,
m1_filter_2(sK210,sK208),
inference(cnf_transformation,[],[f40897]) ).
fof(f42890,plain,
sK209 = sK210,
inference(cnf_transformation,[],[f40897]) ).
fof(f42891,plain,
g3_lattices(u1_struct_0(sK207),u2_lattices(sK207),u1_lattices(sK207)) = g3_lattices(u1_struct_0(sK208),u2_lattices(sK208),u1_lattices(sK208)),
inference(cnf_transformation,[],[f40897]) ).
fof(f42892,plain,
k8_filter_0(sK207,sK209) != k8_filter_0(sK208,sK210),
inference(cnf_transformation,[],[f40897]) ).
fof(f42900,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f40900]) ).
fof(f42913,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = k1_lattice2(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35061]) ).
fof(f42914,plain,
! [X0,X1] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| k1_lattice2(X0) = k1_lattice2(X1)
| ~ l3_lattices(X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35063]) ).
fof(f42951,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35110]) ).
fof(f42952,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u2_lattices(X0) = u1_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35110]) ).
fof(f42995,plain,
! [X0,X1] :
( l3_lattices(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f35150]) ).
fof(f42996,plain,
! [X0,X1] :
( v10_lattices(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f35150]) ).
fof(f42997,plain,
! [X0,X1] :
( ~ v3_struct_0(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f35150]) ).
fof(f43019,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| k1_realset1(u1_lattices(X0),X1) = u1_lattices(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35176]) ).
fof(f43020,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| k1_realset1(u2_lattices(X0),X1) = u2_lattices(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35176]) ).
fof(f43021,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| u1_struct_0(k8_filter_0(X0,X1)) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35176]) ).
fof(f43043,plain,
! [X0,X1] :
( v3_lattices(k8_filter_0(X1,X0))
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f40911]) ).
fof(f43044,plain,
! [X0,X1] :
( ~ v3_struct_0(k8_filter_0(X1,X0))
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f40911]) ).
fof(f43045,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| sP2(X1,X0) ),
inference(cnf_transformation,[],[f40599]) ).
fof(f43146,plain,
! [X0] :
( ~ v3_lattices(X0)
| v3_struct_0(X0)
| k1_lattice2(k1_lattice2(X0)) = X0
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35235]) ).
fof(f51177,plain,
k8_filter_0(sK208,sK210) != k8_filter_0(sK207,sK210),
inference(definition_unfolding,[],[f42892,f42890]) ).
fof(f51178,plain,
m1_filter_2(sK210,sK207),
inference(definition_unfolding,[],[f42888,f42890]) ).
fof(f53666,plain,
( v3_struct_0(sK207)
| g3_lattices(u1_struct_0(sK207),u2_lattices(sK207),u1_lattices(sK207)) = k1_lattice2(k1_lattice2(sK207))
| ~ l3_lattices(sK207) ),
inference(resolution,[],[f42883,f42913]) ).
fof(f53667,plain,
( g3_lattices(u1_struct_0(sK207),u2_lattices(sK207),u1_lattices(sK207)) = k1_lattice2(k1_lattice2(sK207))
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f53666,f42884]) ).
fof(f53668,plain,
g3_lattices(u1_struct_0(sK207),u2_lattices(sK207),u1_lattices(sK207)) = k1_lattice2(k1_lattice2(sK207)),
inference(forward_subsumption_resolution,[],[f53667,f42882]) ).
fof(f53672,plain,
( m1_filter_0(sK210,sK207)
| v3_struct_0(sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207) ),
inference(resolution,[],[f42900,f51178]) ).
fof(f53673,plain,
( m1_filter_0(sK210,sK208)
| v3_struct_0(sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208) ),
inference(resolution,[],[f42900,f42889]) ).
fof(f53681,plain,
( v3_struct_0(sK207)
| u1_lattices(sK207) = u2_lattices(k1_lattice2(sK207)) ),
inference(resolution,[],[f42951,f42882]) ).
fof(f53682,plain,
( v3_struct_0(sK208)
| u1_lattices(sK208) = u2_lattices(k1_lattice2(sK208)) ),
inference(resolution,[],[f42951,f42885]) ).
fof(f53683,plain,
u1_lattices(sK208) = u2_lattices(k1_lattice2(sK208)),
inference(forward_subsumption_resolution,[],[f53682,f42887]) ).
fof(f53684,plain,
u1_lattices(sK207) = u2_lattices(k1_lattice2(sK207)),
inference(forward_subsumption_resolution,[],[f53681,f42884]) ).
fof(f53686,plain,
( v3_struct_0(sK207)
| u2_lattices(sK207) = u1_lattices(k1_lattice2(sK207)) ),
inference(resolution,[],[f42952,f42882]) ).
fof(f53687,plain,
( v3_struct_0(sK208)
| u2_lattices(sK208) = u1_lattices(k1_lattice2(sK208)) ),
inference(resolution,[],[f42952,f42885]) ).
fof(f53688,plain,
u2_lattices(sK208) = u1_lattices(k1_lattice2(sK208)),
inference(forward_subsumption_resolution,[],[f53687,f42887]) ).
fof(f53689,plain,
u2_lattices(sK207) = u1_lattices(k1_lattice2(sK207)),
inference(forward_subsumption_resolution,[],[f53686,f42884]) ).
fof(f53699,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK207),u2_lattices(sK207),u1_lattices(sK207))
| k1_lattice2(X0) = k1_lattice2(sK208)
| ~ l3_lattices(sK208)
| ~ l3_lattices(X0) ),
inference(superposition,[],[f42914,f42891]) ).
fof(f53702,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK207),u2_lattices(sK207),u1_lattices(sK207))
| k1_lattice2(X0) = k1_lattice2(sK208)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f53699,f42885]) ).
fof(f53712,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k1_lattice2(k1_lattice2(sK207))
| k1_lattice2(X0) = k1_lattice2(sK208)
| ~ l3_lattices(X0) ),
inference(forward_demodulation,[],[f53702,f53668]) ).
fof(f53964,plain,
( k1_lattice2(k1_lattice2(sK207)) != k1_lattice2(k1_lattice2(sK207))
| k1_lattice2(sK207) = k1_lattice2(sK208)
| ~ l3_lattices(sK207) ),
inference(superposition,[],[f53712,f53668]) ).
fof(f53965,plain,
( k1_lattice2(sK207) = k1_lattice2(sK208)
| ~ l3_lattices(sK207) ),
inference(trivial_inequality_removal,[],[f53964]) ).
fof(f53966,plain,
k1_lattice2(sK207) = k1_lattice2(sK208),
inference(forward_subsumption_resolution,[],[f53965,f42882]) ).
fof(f53969,plain,
u1_lattices(sK208) = u2_lattices(k1_lattice2(sK207)),
inference(superposition,[],[f53683,f53966]) ).
fof(f53970,plain,
u2_lattices(sK208) = u1_lattices(k1_lattice2(sK207)),
inference(superposition,[],[f53688,f53966]) ).
fof(f53977,plain,
u2_lattices(sK207) = u2_lattices(sK208),
inference(forward_demodulation,[],[f53970,f53689]) ).
fof(f53978,plain,
u1_lattices(sK207) = u1_lattices(sK208),
inference(forward_demodulation,[],[f53969,f53684]) ).
fof(f54533,plain,
! [X0,X1] :
( v3_struct_0(k8_filter_0(X0,X1))
| k8_filter_0(X0,X1) = k1_lattice2(k1_lattice2(k8_filter_0(X0,X1)))
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ sP2(X1,X0) ),
inference(resolution,[],[f43146,f43043]) ).
fof(f54534,plain,
! [X0,X1] :
( ~ l3_lattices(k8_filter_0(X0,X1))
| k8_filter_0(X0,X1) = k1_lattice2(k1_lattice2(k8_filter_0(X0,X1)))
| ~ sP2(X1,X0) ),
inference(forward_subsumption_resolution,[],[f54533,f43044]) ).
fof(f54535,plain,
! [X0,X1] :
( k8_filter_0(X0,X1) = k1_lattice2(k1_lattice2(k8_filter_0(X0,X1)))
| ~ sP2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(resolution,[],[f54534,f42995]) ).
fof(f55198,plain,
( m1_filter_0(sK210,sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208) ),
inference(forward_subsumption_resolution,[],[f53673,f42887]) ).
fof(f55199,plain,
( m1_filter_0(sK210,sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f53672,f42884]) ).
fof(f55319,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k8_filter_0(X0,X1) = k1_lattice2(k1_lattice2(k8_filter_0(X0,X1))) ),
inference(forward_subsumption_resolution,[],[f54535,f43045]) ).
fof(f55459,plain,
( m1_filter_0(sK210,sK208)
| ~ l3_lattices(sK208) ),
inference(forward_subsumption_resolution,[],[f55198,f42886]) ).
fof(f55460,plain,
( m1_filter_0(sK210,sK207)
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f55199,f42883]) ).
fof(f55709,plain,
m1_filter_0(sK210,sK208),
inference(forward_subsumption_resolution,[],[f55459,f42885]) ).
fof(f55710,plain,
m1_filter_0(sK210,sK207),
inference(forward_subsumption_resolution,[],[f55460,f42882]) ).
fof(f57196,plain,
( k1_realset1(u1_lattices(sK207),sK210) = u1_lattices(k8_filter_0(sK207,sK210))
| v3_struct_0(sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207) ),
inference(resolution,[],[f55710,f43019]) ).
fof(f57197,plain,
( k1_realset1(u2_lattices(sK207),sK210) = u2_lattices(k8_filter_0(sK207,sK210))
| v3_struct_0(sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207) ),
inference(resolution,[],[f55710,f43020]) ).
fof(f57198,plain,
( sK210 = u1_struct_0(k8_filter_0(sK207,sK210))
| v3_struct_0(sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207) ),
inference(resolution,[],[f55710,f43021]) ).
fof(f57202,plain,
( v3_struct_0(sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207)
| k8_filter_0(sK207,sK210) = k1_lattice2(k1_lattice2(k8_filter_0(sK207,sK210))) ),
inference(resolution,[],[f55710,f55319]) ).
fof(f57203,plain,
( ~ v10_lattices(sK207)
| ~ l3_lattices(sK207)
| k8_filter_0(sK207,sK210) = k1_lattice2(k1_lattice2(k8_filter_0(sK207,sK210))) ),
inference(forward_subsumption_resolution,[],[f57202,f42884]) ).
fof(f57205,plain,
( sK210 = u1_struct_0(k8_filter_0(sK207,sK210))
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f57198,f42884]) ).
fof(f57206,plain,
( k1_realset1(u2_lattices(sK207),sK210) = u2_lattices(k8_filter_0(sK207,sK210))
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f57197,f42884]) ).
fof(f57207,plain,
( k1_realset1(u1_lattices(sK207),sK210) = u1_lattices(k8_filter_0(sK207,sK210))
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f57196,f42884]) ).
fof(f57208,plain,
( ~ l3_lattices(sK207)
| k8_filter_0(sK207,sK210) = k1_lattice2(k1_lattice2(k8_filter_0(sK207,sK210))) ),
inference(forward_subsumption_resolution,[],[f57203,f42883]) ).
fof(f57210,plain,
( sK210 = u1_struct_0(k8_filter_0(sK207,sK210))
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f57205,f42883]) ).
fof(f57211,plain,
( k1_realset1(u2_lattices(sK207),sK210) = u2_lattices(k8_filter_0(sK207,sK210))
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f57206,f42883]) ).
fof(f57212,plain,
( k1_realset1(u1_lattices(sK207),sK210) = u1_lattices(k8_filter_0(sK207,sK210))
| ~ l3_lattices(sK207) ),
inference(forward_subsumption_resolution,[],[f57207,f42883]) ).
fof(f57213,plain,
k8_filter_0(sK207,sK210) = k1_lattice2(k1_lattice2(k8_filter_0(sK207,sK210))),
inference(forward_subsumption_resolution,[],[f57208,f42882]) ).
fof(f57215,plain,
sK210 = u1_struct_0(k8_filter_0(sK207,sK210)),
inference(forward_subsumption_resolution,[],[f57210,f42882]) ).
fof(f57216,plain,
k1_realset1(u2_lattices(sK207),sK210) = u2_lattices(k8_filter_0(sK207,sK210)),
inference(forward_subsumption_resolution,[],[f57211,f42882]) ).
fof(f57217,plain,
k1_realset1(u1_lattices(sK207),sK210) = u1_lattices(k8_filter_0(sK207,sK210)),
inference(forward_subsumption_resolution,[],[f57212,f42882]) ).
fof(f57243,definition,
( spl1434_91
<=> l3_lattices(k8_filter_0(sK207,sK210)) ),
introduced(definition,[new_symbols(definition,[spl1434_91])],[avatar_definition]) ).
fof(f57244,plain,
( ~ l3_lattices(k8_filter_0(sK207,sK210))
| spl1434_91 ),
inference(avatar_component_clause,[],[f57243]) ).
fof(f57245,plain,
( l3_lattices(k8_filter_0(sK207,sK210))
| ~ spl1434_91 ),
inference(avatar_component_clause,[],[f57243]) ).
fof(f57248,definition,
( spl1434_92
<=> v3_struct_0(k8_filter_0(sK207,sK210)) ),
introduced(definition,[new_symbols(definition,[spl1434_92])],[avatar_definition]) ).
fof(f57249,plain,
( v3_struct_0(k8_filter_0(sK207,sK210))
| ~ spl1434_92 ),
inference(avatar_component_clause,[],[f57248]) ).
fof(f57250,plain,
( ~ v3_struct_0(k8_filter_0(sK207,sK210))
| spl1434_92 ),
inference(avatar_component_clause,[],[f57248]) ).
fof(f57257,definition,
( spl1434_94
<=> v10_lattices(k8_filter_0(sK207,sK210)) ),
introduced(definition,[new_symbols(definition,[spl1434_94])],[avatar_definition]) ).
fof(f57258,plain,
( ~ v10_lattices(k8_filter_0(sK207,sK210))
| spl1434_94 ),
inference(avatar_component_clause,[],[f57257]) ).
fof(f57259,plain,
( v10_lattices(k8_filter_0(sK207,sK210))
| ~ spl1434_94 ),
inference(avatar_component_clause,[],[f57257]) ).
fof(f57522,plain,
( v3_struct_0(sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| spl1434_91 ),
inference(resolution,[],[f57244,f42995]) ).
fof(f57523,plain,
( ~ v10_lattices(sK207)
| ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| spl1434_91 ),
inference(forward_subsumption_resolution,[],[f57522,f42884]) ).
fof(f57524,plain,
( ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| spl1434_91 ),
inference(forward_subsumption_resolution,[],[f57523,f42883]) ).
fof(f57525,plain,
( ~ m1_filter_0(sK210,sK207)
| spl1434_91 ),
inference(forward_subsumption_resolution,[],[f57524,f42882]) ).
fof(f57526,plain,
( $false
| spl1434_91 ),
inference(forward_subsumption_resolution,[],[f57525,f55710]) ).
fof(f57527,plain,
spl1434_91,
inference(avatar_contradiction_clause,[],[f57526]) ).
fof(f57529,plain,
( v3_struct_0(sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| ~ spl1434_92 ),
inference(resolution,[],[f57249,f42997]) ).
fof(f57530,plain,
( ~ v10_lattices(sK207)
| ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| ~ spl1434_92 ),
inference(forward_subsumption_resolution,[],[f57529,f42884]) ).
fof(f57533,plain,
( ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| ~ spl1434_92 ),
inference(forward_subsumption_resolution,[],[f57530,f42883]) ).
fof(f57534,plain,
( ~ m1_filter_0(sK210,sK207)
| ~ spl1434_92 ),
inference(forward_subsumption_resolution,[],[f57533,f42882]) ).
fof(f57535,plain,
( $false
| ~ spl1434_92 ),
inference(forward_subsumption_resolution,[],[f57534,f55710]) ).
fof(f57536,plain,
~ spl1434_92,
inference(avatar_contradiction_clause,[],[f57535]) ).
fof(f57538,plain,
( v3_struct_0(sK207)
| ~ v10_lattices(sK207)
| ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| spl1434_94 ),
inference(resolution,[],[f57258,f42996]) ).
fof(f57539,plain,
( ~ v10_lattices(sK207)
| ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| spl1434_94 ),
inference(forward_subsumption_resolution,[],[f57538,f42884]) ).
fof(f57542,plain,
( ~ l3_lattices(sK207)
| ~ m1_filter_0(sK210,sK207)
| spl1434_94 ),
inference(forward_subsumption_resolution,[],[f57539,f42883]) ).
fof(f57543,plain,
( ~ m1_filter_0(sK210,sK207)
| spl1434_94 ),
inference(forward_subsumption_resolution,[],[f57542,f42882]) ).
fof(f57544,plain,
( $false
| spl1434_94 ),
inference(forward_subsumption_resolution,[],[f57543,f55710]) ).
fof(f57545,plain,
spl1434_94,
inference(avatar_contradiction_clause,[],[f57544]) ).
fof(f57550,plain,
( v3_struct_0(k8_filter_0(sK207,sK210))
| k1_lattice2(k1_lattice2(k8_filter_0(sK207,sK210))) = g3_lattices(u1_struct_0(k8_filter_0(sK207,sK210)),u2_lattices(k8_filter_0(sK207,sK210)),u1_lattices(k8_filter_0(sK207,sK210)))
| ~ l3_lattices(k8_filter_0(sK207,sK210))
| ~ spl1434_94 ),
inference(resolution,[],[f57259,f42913]) ).
fof(f57551,plain,
( k1_lattice2(k1_lattice2(k8_filter_0(sK207,sK210))) = g3_lattices(u1_struct_0(k8_filter_0(sK207,sK210)),u2_lattices(k8_filter_0(sK207,sK210)),u1_lattices(k8_filter_0(sK207,sK210)))
| ~ l3_lattices(k8_filter_0(sK207,sK210))
| spl1434_92
| ~ spl1434_94 ),
inference(forward_subsumption_resolution,[],[f57550,f57250]) ).
fof(f57556,plain,
( k1_lattice2(k1_lattice2(k8_filter_0(sK207,sK210))) = g3_lattices(u1_struct_0(k8_filter_0(sK207,sK210)),u2_lattices(k8_filter_0(sK207,sK210)),u1_lattices(k8_filter_0(sK207,sK210)))
| ~ spl1434_91
| spl1434_92
| ~ spl1434_94 ),
inference(forward_subsumption_resolution,[],[f57551,f57245]) ).
fof(f57561,plain,
( k1_lattice2(k1_lattice2(k8_filter_0(sK207,sK210))) = g3_lattices(sK210,u2_lattices(k8_filter_0(sK207,sK210)),u1_lattices(k8_filter_0(sK207,sK210)))
| ~ spl1434_91
| spl1434_92
| ~ spl1434_94 ),
inference(forward_demodulation,[],[f57556,f57215]) ).
fof(f57564,plain,
( k8_filter_0(sK207,sK210) = g3_lattices(sK210,u2_lattices(k8_filter_0(sK207,sK210)),u1_lattices(k8_filter_0(sK207,sK210)))
| ~ spl1434_91
| spl1434_92
| ~ spl1434_94 ),
inference(forward_demodulation,[],[f57561,f57213]) ).
fof(f57571,plain,
( k1_realset1(u1_lattices(sK208),sK210) = u1_lattices(k8_filter_0(sK208,sK210))
| v3_struct_0(sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208) ),
inference(resolution,[],[f55709,f43019]) ).
fof(f57572,plain,
( k1_realset1(u2_lattices(sK208),sK210) = u2_lattices(k8_filter_0(sK208,sK210))
| v3_struct_0(sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208) ),
inference(resolution,[],[f55709,f43020]) ).
fof(f57573,plain,
( sK210 = u1_struct_0(k8_filter_0(sK208,sK210))
| v3_struct_0(sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208) ),
inference(resolution,[],[f55709,f43021]) ).
fof(f57577,plain,
( v3_struct_0(sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208)
| k8_filter_0(sK208,sK210) = k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))) ),
inference(resolution,[],[f55709,f55319]) ).
fof(f57578,plain,
( ~ v10_lattices(sK208)
| ~ l3_lattices(sK208)
| k8_filter_0(sK208,sK210) = k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))) ),
inference(forward_subsumption_resolution,[],[f57577,f42887]) ).
fof(f57580,plain,
( sK210 = u1_struct_0(k8_filter_0(sK208,sK210))
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208) ),
inference(forward_subsumption_resolution,[],[f57573,f42887]) ).
fof(f57581,plain,
( k1_realset1(u2_lattices(sK208),sK210) = u2_lattices(k8_filter_0(sK208,sK210))
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208) ),
inference(forward_subsumption_resolution,[],[f57572,f42887]) ).
fof(f57582,plain,
( k1_realset1(u1_lattices(sK208),sK210) = u1_lattices(k8_filter_0(sK208,sK210))
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208) ),
inference(forward_subsumption_resolution,[],[f57571,f42887]) ).
fof(f57583,plain,
( ~ l3_lattices(sK208)
| k8_filter_0(sK208,sK210) = k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))) ),
inference(forward_subsumption_resolution,[],[f57578,f42886]) ).
fof(f57585,plain,
( sK210 = u1_struct_0(k8_filter_0(sK208,sK210))
| ~ l3_lattices(sK208) ),
inference(forward_subsumption_resolution,[],[f57580,f42886]) ).
fof(f57586,plain,
( k1_realset1(u2_lattices(sK208),sK210) = u2_lattices(k8_filter_0(sK208,sK210))
| ~ l3_lattices(sK208) ),
inference(forward_subsumption_resolution,[],[f57581,f42886]) ).
fof(f57587,plain,
( k1_realset1(u1_lattices(sK208),sK210) = u1_lattices(k8_filter_0(sK208,sK210))
| ~ l3_lattices(sK208) ),
inference(forward_subsumption_resolution,[],[f57582,f42886]) ).
fof(f57588,plain,
k8_filter_0(sK208,sK210) = k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))),
inference(forward_subsumption_resolution,[],[f57583,f42885]) ).
fof(f57590,plain,
sK210 = u1_struct_0(k8_filter_0(sK208,sK210)),
inference(forward_subsumption_resolution,[],[f57585,f42885]) ).
fof(f57591,plain,
k1_realset1(u2_lattices(sK208),sK210) = u2_lattices(k8_filter_0(sK208,sK210)),
inference(forward_subsumption_resolution,[],[f57586,f42885]) ).
fof(f57592,plain,
k1_realset1(u1_lattices(sK208),sK210) = u1_lattices(k8_filter_0(sK208,sK210)),
inference(forward_subsumption_resolution,[],[f57587,f42885]) ).
fof(f57593,plain,
k1_realset1(u2_lattices(sK207),sK210) = u2_lattices(k8_filter_0(sK208,sK210)),
inference(forward_demodulation,[],[f57591,f53977]) ).
fof(f57594,plain,
k1_realset1(u1_lattices(sK207),sK210) = u1_lattices(k8_filter_0(sK208,sK210)),
inference(forward_demodulation,[],[f57592,f53978]) ).
fof(f57595,plain,
u2_lattices(k8_filter_0(sK207,sK210)) = u2_lattices(k8_filter_0(sK208,sK210)),
inference(forward_demodulation,[],[f57593,f57216]) ).
fof(f57596,plain,
u1_lattices(k8_filter_0(sK207,sK210)) = u1_lattices(k8_filter_0(sK208,sK210)),
inference(forward_demodulation,[],[f57594,f57217]) ).
fof(f57622,definition,
( spl1434_145
<=> l3_lattices(k8_filter_0(sK208,sK210)) ),
introduced(definition,[new_symbols(definition,[spl1434_145])],[avatar_definition]) ).
fof(f57623,plain,
( ~ l3_lattices(k8_filter_0(sK208,sK210))
| spl1434_145 ),
inference(avatar_component_clause,[],[f57622]) ).
fof(f57624,plain,
( l3_lattices(k8_filter_0(sK208,sK210))
| ~ spl1434_145 ),
inference(avatar_component_clause,[],[f57622]) ).
fof(f57627,definition,
( spl1434_146
<=> v3_struct_0(k8_filter_0(sK208,sK210)) ),
introduced(definition,[new_symbols(definition,[spl1434_146])],[avatar_definition]) ).
fof(f57628,plain,
( v3_struct_0(k8_filter_0(sK208,sK210))
| ~ spl1434_146 ),
inference(avatar_component_clause,[],[f57627]) ).
fof(f57629,plain,
( ~ v3_struct_0(k8_filter_0(sK208,sK210))
| spl1434_146 ),
inference(avatar_component_clause,[],[f57627]) ).
fof(f57636,definition,
( spl1434_148
<=> v10_lattices(k8_filter_0(sK208,sK210)) ),
introduced(definition,[new_symbols(definition,[spl1434_148])],[avatar_definition]) ).
fof(f57637,plain,
( ~ v10_lattices(k8_filter_0(sK208,sK210))
| spl1434_148 ),
inference(avatar_component_clause,[],[f57636]) ).
fof(f57638,plain,
( v10_lattices(k8_filter_0(sK208,sK210))
| ~ spl1434_148 ),
inference(avatar_component_clause,[],[f57636]) ).
fof(f57905,plain,
( v3_struct_0(sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| spl1434_145 ),
inference(resolution,[],[f57623,f42995]) ).
fof(f57906,plain,
( ~ v10_lattices(sK208)
| ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| spl1434_145 ),
inference(forward_subsumption_resolution,[],[f57905,f42887]) ).
fof(f57907,plain,
( ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| spl1434_145 ),
inference(forward_subsumption_resolution,[],[f57906,f42886]) ).
fof(f57908,plain,
( ~ m1_filter_0(sK210,sK208)
| spl1434_145 ),
inference(forward_subsumption_resolution,[],[f57907,f42885]) ).
fof(f57909,plain,
( $false
| spl1434_145 ),
inference(forward_subsumption_resolution,[],[f57908,f55709]) ).
fof(f57910,plain,
spl1434_145,
inference(avatar_contradiction_clause,[],[f57909]) ).
fof(f57912,plain,
( v3_struct_0(sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| ~ spl1434_146 ),
inference(resolution,[],[f57628,f42997]) ).
fof(f57913,plain,
( ~ v10_lattices(sK208)
| ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| ~ spl1434_146 ),
inference(forward_subsumption_resolution,[],[f57912,f42887]) ).
fof(f57916,plain,
( ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| ~ spl1434_146 ),
inference(forward_subsumption_resolution,[],[f57913,f42886]) ).
fof(f57917,plain,
( ~ m1_filter_0(sK210,sK208)
| ~ spl1434_146 ),
inference(forward_subsumption_resolution,[],[f57916,f42885]) ).
fof(f57918,plain,
( $false
| ~ spl1434_146 ),
inference(forward_subsumption_resolution,[],[f57917,f55709]) ).
fof(f57919,plain,
~ spl1434_146,
inference(avatar_contradiction_clause,[],[f57918]) ).
fof(f57921,plain,
( v3_struct_0(sK208)
| ~ v10_lattices(sK208)
| ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| spl1434_148 ),
inference(resolution,[],[f57637,f42996]) ).
fof(f57922,plain,
( ~ v10_lattices(sK208)
| ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| spl1434_148 ),
inference(forward_subsumption_resolution,[],[f57921,f42887]) ).
fof(f57925,plain,
( ~ l3_lattices(sK208)
| ~ m1_filter_0(sK210,sK208)
| spl1434_148 ),
inference(forward_subsumption_resolution,[],[f57922,f42886]) ).
fof(f57926,plain,
( ~ m1_filter_0(sK210,sK208)
| spl1434_148 ),
inference(forward_subsumption_resolution,[],[f57925,f42885]) ).
fof(f57927,plain,
( $false
| spl1434_148 ),
inference(forward_subsumption_resolution,[],[f57926,f55709]) ).
fof(f57928,plain,
spl1434_148,
inference(avatar_contradiction_clause,[],[f57927]) ).
fof(f57933,plain,
( v3_struct_0(k8_filter_0(sK208,sK210))
| k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))) = g3_lattices(u1_struct_0(k8_filter_0(sK208,sK210)),u2_lattices(k8_filter_0(sK208,sK210)),u1_lattices(k8_filter_0(sK208,sK210)))
| ~ l3_lattices(k8_filter_0(sK208,sK210))
| ~ spl1434_148 ),
inference(resolution,[],[f57638,f42913]) ).
fof(f57934,plain,
( k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))) = g3_lattices(u1_struct_0(k8_filter_0(sK208,sK210)),u2_lattices(k8_filter_0(sK208,sK210)),u1_lattices(k8_filter_0(sK208,sK210)))
| ~ l3_lattices(k8_filter_0(sK208,sK210))
| spl1434_146
| ~ spl1434_148 ),
inference(forward_subsumption_resolution,[],[f57933,f57629]) ).
fof(f57939,plain,
( k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))) = g3_lattices(u1_struct_0(k8_filter_0(sK208,sK210)),u2_lattices(k8_filter_0(sK208,sK210)),u1_lattices(k8_filter_0(sK208,sK210)))
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(forward_subsumption_resolution,[],[f57934,f57624]) ).
fof(f57944,plain,
( k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))) = g3_lattices(u1_struct_0(k8_filter_0(sK208,sK210)),u2_lattices(k8_filter_0(sK208,sK210)),u1_lattices(k8_filter_0(sK207,sK210)))
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(forward_demodulation,[],[f57939,f57596]) ).
fof(f57947,plain,
( k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210))) = g3_lattices(u1_struct_0(k8_filter_0(sK208,sK210)),u2_lattices(k8_filter_0(sK207,sK210)),u1_lattices(k8_filter_0(sK207,sK210)))
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(forward_demodulation,[],[f57944,f57595]) ).
fof(f57948,plain,
( g3_lattices(sK210,u2_lattices(k8_filter_0(sK207,sK210)),u1_lattices(k8_filter_0(sK207,sK210))) = k1_lattice2(k1_lattice2(k8_filter_0(sK208,sK210)))
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(forward_demodulation,[],[f57947,f57590]) ).
fof(f57949,plain,
( k8_filter_0(sK208,sK210) = g3_lattices(sK210,u2_lattices(k8_filter_0(sK207,sK210)),u1_lattices(k8_filter_0(sK207,sK210)))
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(forward_demodulation,[],[f57948,f57588]) ).
fof(f57950,plain,
( k8_filter_0(sK208,sK210) = k8_filter_0(sK207,sK210)
| ~ spl1434_91
| spl1434_92
| ~ spl1434_94
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(forward_demodulation,[],[f57949,f57564]) ).
fof(f57951,plain,
( $false
| ~ spl1434_91
| spl1434_92
| ~ spl1434_94
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(forward_subsumption_resolution,[],[f57950,f51177]) ).
fof(f57952,plain,
( ~ spl1434_91
| spl1434_92
| ~ spl1434_94
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(avatar_contradiction_clause,[],[f57951]) ).
cnf(s258,plain,
spl1434_91,
inference(sat_conversion,[],[f57527]) ).
cnf(s260,plain,
~ spl1434_92,
inference(sat_conversion,[],[f57536]) ).
cnf(s262,plain,
spl1434_94,
inference(sat_conversion,[],[f57545]) ).
cnf(s301,plain,
spl1434_145,
inference(sat_conversion,[],[f57910]) ).
cnf(s303,plain,
~ spl1434_146,
inference(sat_conversion,[],[f57919]) ).
cnf(s305,plain,
spl1434_148,
inference(sat_conversion,[],[f57928]) ).
cnf(s306,plain,
( ~ spl1434_91
| spl1434_92
| ~ spl1434_94
| ~ spl1434_145
| spl1434_146
| ~ spl1434_148 ),
inference(sat_conversion,[],[f57952]) ).
cnf(s335,plain,
~ spl1434_91,
inference(rat,[],[s306,s305,s303,s301,s262,s260]) ).
cnf(s336,plain,
$false,
inference(rat,[],[s258,s335]) ).
fof(f57953,plain,
$false,
inference(avatar_sat_refutation,[],[s336]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT331+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 14:40:32 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/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
% 14.49/5.01 % (1489954)Detected formulas, will run a generic FOF schedule.
% 14.49/5.01 % (1489964)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3508338918:s2a=on:i=139:gtg=position_2977 on theBenchmark for (2977ds/139Mi)
% 14.49/5.01 % (1489959)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=2843252180:i=141193_2977 on theBenchmark for (2977ds/141193Mi)
% 14.49/5.01 % (1489961)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=628151121:i=141695:sd=1:nm=32:gsp=on:ss=included_2977 on theBenchmark for (2977ds/141695Mi)
% 14.49/5.01 % (1489962)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2242890668:i=109:sd=1:ins=1:gsp=on:ss=axioms_2977 on theBenchmark for (2977ds/109Mi)
% 14.49/5.01 % (1489963)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2625060382:i=119:av=off:ss=axioms_2977 on theBenchmark for (2977ds/119Mi)
% 14.49/5.01 % (1489960)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=1406472793:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2977 on theBenchmark for (2977ds/134677Mi)
% 14.49/5.01 % (1489964)Instruction limit reached!
% 14.49/5.01 % (1489964)------------------------------
% 14.49/5.01 % (1489964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/5.01 % (1489964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/5.01 % (1489964)CaDiCaL version: 2.1.3
% 14.49/5.01 % (1489964)Termination reason: Instruction limit
% 14.49/5.01 % (1489964)Termination phase: Property scanning
% 14.49/5.01 % (1489964)Time elapsed: 0.035 s
% 14.49/5.01 % (1489964)Peak memory usage: 136 MB
% 14.49/5.01 % (1489964)Instructions burned: 139 (million)
% 14.49/5.01 % (1489965)dis-21_1_sil=8000:lcm=predicate:random_seed=3249154056:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2977 on theBenchmark for (2977ds/129Mi)
% 14.49/5.01 % (1489962)Instruction limit reached!
% 14.49/5.01 % (1489962)------------------------------
% 14.49/5.01 % (1489962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/5.01 % (1489962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/5.01 % (1489962)CaDiCaL version: 2.1.3
% 14.49/5.01 % (1489962)Termination reason: Instruction limit
% 14.49/5.01 % (1489962)Termination phase: SInE selection
% 14.49/5.01 % (1489962)Time elapsed: 0.084 s
% 14.49/5.01 % (1489962)Peak memory usage: 136 MB
% 14.49/5.01 % (1489962)Instructions burned: 110 (million)
% 14.49/5.01 % (1489963)Instruction limit reached!
% 14.49/5.01 % (1489963)------------------------------
% 14.49/5.01 % (1489963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/5.01 % (1489963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/5.01 % (1489963)CaDiCaL version: 2.1.3
% 14.49/5.01 % (1489963)Termination reason: Instruction limit
% 14.49/5.01 % (1489963)Termination phase: SInE selection
% 14.49/5.01 % (1489963)Time elapsed: 0.091 s
% 14.49/5.01 % (1489963)Peak memory usage: 136 MB
% 14.49/5.01 % (1489963)Instructions burned: 120 (million)
% 14.49/5.01 % (1489965)Instruction limit reached!
% 14.49/5.01 % (1489965)------------------------------
% 14.49/5.01 % (1489965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/5.01 % (1489965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/5.01 % (1489965)CaDiCaL version: 2.1.3
% 14.49/5.01 % (1489965)Termination reason: Instruction limit
% 14.49/5.01 % (1489965)Termination phase: SInE selection
% 14.49/5.01 % (1489965)Time elapsed: 0.099 s
% 14.49/5.01 % (1489965)Peak memory usage: 136 MB
% 14.49/5.01 % (1489965)Instructions burned: 130 (million)
% 14.49/5.01 % (1489972)lrs+10_1_sil=8000:sp=occurrence:random_seed=3196215185:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 14.49/5.01 % (1489974)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2497747618:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 14.49/5.01 % (1489975)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2762919568:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 14.49/5.01 % (1489972)Instruction limit reached!
% 14.49/5.01 % (1489972)------------------------------
% 14.49/5.01 % (1489972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/5.01 % (1489972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.66/6.29 % (1489972)CaDiCaL version: 2.1.3
% 24.66/6.29 % (1489972)Termination reason: Instruction limit
% 24.66/6.29 % (1489972)Termination phase: Saturation
% 24.66/6.29 % (1489972)Time elapsed: 0.129 s
% 24.66/6.29 % (1489972)Peak memory usage: 141 MB
% 24.66/6.29 % (1489972)Instructions burned: 288 (million)
% 24.66/6.29 % (1489976)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=2263281464:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 24.66/6.29 % (1489974)Instruction limit reached!
% 24.66/6.29 % (1489974)------------------------------
% 24.66/6.29 % (1489974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.66/6.29 % (1489974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.66/6.29 % (1489974)CaDiCaL version: 2.1.3
% 24.66/6.29 % (1489974)Termination reason: Instruction limit
% 24.66/6.29 % (1489974)Termination phase: Property scanning
% 24.66/6.29 % (1489974)Time elapsed: 0.069 s
% 24.66/6.29 % (1489974)Peak memory usage: 136 MB
% 24.66/6.29 % (1489974)Instructions burned: 158 (million)
% 24.66/6.29 % (1489976)Instruction limit reached!
% 24.66/6.29 % (1489976)------------------------------
% 24.66/6.29 % (1489976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.66/6.29 % (1489976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.66/6.29 % (1489976)CaDiCaL version: 2.1.3
% 24.66/6.29 % (1489976)Termination reason: Instruction limit
% 24.66/6.29 % (1489976)Termination phase: Property scanning
% 24.66/6.29 % (1489976)Time elapsed: 0.107 s
% 24.66/6.29 % (1489976)Peak memory usage: 136 MB
% 24.66/6.29 % (1489976)Instructions burned: 249 (million)
% 24.66/6.29 % (1489980)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3318050654:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 24.66/6.29 % (1489982)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=629862453:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 24.66/6.29 % (1489975)Instruction limit reached!
% 24.66/6.29 % (1489975)------------------------------
% 24.66/6.29 % (1489975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.66/6.29 % (1489975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.66/6.29 % (1489975)CaDiCaL version: 2.1.3
% 24.66/6.29 % (1489975)Termination reason: Instruction limit
% 24.66/6.29 % (1489975)Termination phase: Saturation
% 24.66/6.29 % (1489975)Time elapsed: 0.251 s
% 24.66/6.29 % (1489975)Peak memory usage: 142 MB
% 24.66/6.29 % (1489975)Instructions burned: 326 (million)
% 24.66/6.29 % (1489980)Instruction limit reached!
% 24.66/6.29 % (1489980)------------------------------
% 24.66/6.29 % (1489980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.66/6.29 % (1489980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.66/6.29 % (1489980)CaDiCaL version: 2.1.3
% 24.66/6.29 % (1489980)Termination reason: Instruction limit
% 24.66/6.29 % (1489980)Termination phase: SInE selection
% 24.66/6.29 % (1489980)Time elapsed: 0.110 s
% 24.66/6.29 % (1489980)Peak memory usage: 137 MB
% 24.66/6.29 % (1489980)Instructions burned: 295 (million)
% 24.66/6.29 % (1489983)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1164784985:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 24.66/6.29 % (1489987)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3278409271:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2971 on theBenchmark for (2971ds/114Mi)
% 24.66/6.29 % (1489983)Instruction limit reached!
% 24.66/6.29 % (1489983)------------------------------
% 24.66/6.29 % (1489983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.66/6.29 % (1489983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.66/6.29 % (1489983)CaDiCaL version: 2.1.3
% 24.66/6.29 % (1489983)Termination reason: Instruction limit
% 24.66/6.29 % (1489983)Termination phase: SInE selection
% 24.66/6.29 % (1489983)Time elapsed: 0.090 s
% 24.66/6.29 % (1489983)Peak memory usage: 136 MB
% 24.66/6.29 % (1489983)Instructions burned: 113 (million)
% 24.66/6.29 % (1489986)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2112508460:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 24.66/6.29 % (1489987)Instruction limit reached!
% 24.66/6.29 % (1489987)------------------------------
% 24.66/6.29 % (1489987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/8.65 % (1489987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/8.65 % (1489987)CaDiCaL version: 2.1.3
% 41.61/8.65 % (1489987)Termination reason: Instruction limit
% 41.61/8.65 % (1489987)Termination phase: Property scanning
% 41.61/8.65 % (1489987)Time elapsed: 0.029 s
% 41.61/8.65 % (1489987)Peak memory usage: 136 MB
% 41.61/8.65 % (1489987)Instructions burned: 115 (million)
% 41.61/8.65 % (1489986)Instruction limit reached!
% 41.61/8.65 % (1489986)------------------------------
% 41.61/8.65 % (1489986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/8.65 % (1489986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/8.65 % (1489986)CaDiCaL version: 2.1.3
% 41.61/8.65 % (1489986)Termination reason: Instruction limit
% 41.61/8.65 % (1489986)Termination phase: Preprocessing 1
% 41.61/8.65 % (1489986)Time elapsed: 0.098 s
% 41.61/8.65 % (1489986)Peak memory usage: 137 MB
% 41.61/8.65 % (1489986)Instructions burned: 130 (million)
% 41.61/8.65 % (1489991)lrs+10_1_sil=8000:sp=occurrence:random_seed=681049767:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 41.61/8.65 % (1489992)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1045884605:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 41.61/8.65 % (1489993)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4248588089:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 41.61/8.65 % (1489992)Instruction limit reached!
% 41.61/8.65 % (1489992)------------------------------
% 41.61/8.65 % (1489992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/8.65 % (1489992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/8.65 % (1489992)CaDiCaL version: 2.1.3
% 41.61/8.65 % (1489992)Termination reason: Instruction limit
% 41.61/8.65 % (1489992)Termination phase: Saturation
% 41.61/8.65 % (1489992)Time elapsed: 0.177 s
% 41.61/8.65 % (1489992)Peak memory usage: 144 MB
% 41.61/8.65 % (1489992)Instructions burned: 440 (million)
% 41.61/8.65 % (1489997)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=169925575:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2966 on theBenchmark for (2966ds/134Mi)
% 41.61/8.65 % (1489997)Instruction limit reached!
% 41.61/8.65 % (1489997)------------------------------
% 41.61/8.65 % (1489997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/8.65 % (1489997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/8.65 % (1489997)CaDiCaL version: 2.1.3
% 41.61/8.65 % (1489997)Termination reason: Instruction limit
% 41.61/8.65 % (1489997)Termination phase: SInE selection
% 41.61/8.65 % (1489997)Time elapsed: 0.059 s
% 41.61/8.65 % (1489997)Peak memory usage: 136 MB
% 41.61/8.65 % (1489997)Instructions burned: 135 (million)
% 41.61/8.65 % (1489999)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=304112765:st=8:i=592:sd=3:ep=RST:ss=axioms_2964 on theBenchmark for (2964ds/592Mi)
% 41.61/8.65 % (1489991)Instruction limit reached!
% 41.61/8.65 % (1489991)------------------------------
% 41.61/8.65 % (1489991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/8.65 % (1489991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/8.65 % (1489991)CaDiCaL version: 2.1.3
% 41.61/8.65 % (1489991)Termination reason: Instruction limit
% 41.61/8.65 % (1489991)Termination phase: Property scanning
% 41.61/8.65 % (1489991)Time elapsed: 0.600 s
% 41.61/8.65 % (1489991)Peak memory usage: 159 MB
% 41.61/8.65 % (1489991)Instructions burned: 908 (million)
% 41.61/8.65 % (1490001)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2063487458:st=3:i=13193:sd=3:ss=axioms_2962 on theBenchmark for (2962ds/13193Mi)
% 41.61/8.65 % (1489999)Instruction limit reached!
% 41.61/8.65 % (1489999)------------------------------
% 41.61/8.65 % (1489999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.61/8.65 % (1489999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.61/8.65 % (1489999)CaDiCaL version: 2.1.3
% 41.61/8.65 % (1489999)Termination reason: Instruction limit
% 41.61/8.65 % (1489999)Termination phase: Naming
% 41.61/8.65 % (1489999)Time elapsed: 0.271 s
% 41.61/8.65 % (1489999)Peak memory usage: 154 MB
% 41.61/8.65 % (1489999)Instructions burned: 593 (million)
% 41.61/8.65 % (1490003)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=2232278227:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/125Mi)
% 42.13/8.79 % (1490003)Instruction limit reached!
% 42.13/8.79 % (1490003)------------------------------
% 42.13/8.79 % (1490003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490003)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490003)Termination reason: Instruction limit
% 42.13/8.79 % (1490003)Termination phase: Property scanning
% 42.13/8.79 % (1490003)Time elapsed: 0.031 s
% 42.13/8.79 % (1490003)Peak memory usage: 136 MB
% 42.13/8.79 % (1490003)Instructions burned: 127 (million)
% 42.13/8.79 % (1490005)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2792314974:i=134:gtgl=5:slsql=off:gtg=exists_sym_2958 on theBenchmark for (2958ds/134Mi)
% 42.13/8.79 % (1490005)Instruction limit reached!
% 42.13/8.79 % (1490005)------------------------------
% 42.13/8.79 % (1490005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490005)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490005)Termination reason: Instruction limit
% 42.13/8.79 % (1490005)Termination phase: Property scanning
% 42.13/8.79 % (1490005)Time elapsed: 0.034 s
% 42.13/8.79 % (1490005)Peak memory usage: 136 MB
% 42.13/8.79 % (1490005)Instructions burned: 136 (million)
% 42.13/8.79 % (1489982)Instruction limit reached!
% 42.13/8.79 % (1489982)------------------------------
% 42.13/8.79 % (1489982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1489982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1489982)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1489982)Termination reason: Instruction limit
% 42.13/8.79 % (1489982)Termination phase: Property scanning
% 42.13/8.79 % (1489982)Time elapsed: 1.603 s
% 42.13/8.79 % (1489982)Peak memory usage: 233 MB
% 42.13/8.79 % (1489982)Instructions burned: 2353 (million)
% 42.13/8.79 % (1490007)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=892659629:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/141Mi)
% 42.13/8.79 % (1490007)Instruction limit reached!
% 42.13/8.79 % (1490007)------------------------------
% 42.13/8.79 % (1490007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490007)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490007)Termination reason: Instruction limit
% 42.13/8.79 % (1490007)Termination phase: SInE selection
% 42.13/8.79 % (1490007)Time elapsed: 0.063 s
% 42.13/8.79 % (1490007)Peak memory usage: 136 MB
% 42.13/8.79 % (1490007)Instructions burned: 141 (million)
% 42.13/8.79 % (1490008)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3087415486:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2955 on theBenchmark for (2955ds/431Mi)
% 42.13/8.79 % (1490010)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=2422760416:i=6060:aac=none:ins=25_2954 on theBenchmark for (2954ds/6060Mi)
% 42.13/8.79 % (1490008)Refutation not found, incomplete strategy
% 42.13/8.79 % (1490008)------------------------------
% 42.13/8.79 % (1490008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490008)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490008)Termination reason: Refutation not found, incomplete strategy
% 42.13/8.79 % (1490008)Time elapsed: 0.205 s
% 42.13/8.79 % (1490008)Peak memory usage: 142 MB
% 42.13/8.79 % (1490008)Instructions burned: 261 (million)
% 42.13/8.79 % (1490008)------------------------------
% 42.13/8.79 % (1490008)------------------------------
% 42.13/8.79 % (1490013)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=3470621575:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2948 on theBenchmark for (2948ds/150Mi)
% 42.13/8.79 % (1490013)Instruction limit reached!
% 42.13/8.79 % (1490013)------------------------------
% 42.13/8.79 % (1490013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490013)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490013)Termination reason: Instruction limit
% 42.13/8.79 % (1490013)Termination phase: SInE selection
% 42.13/8.79 % (1490013)Time elapsed: 0.116 s
% 42.13/8.79 % (1490013)Peak memory usage: 136 MB
% 42.13/8.79 % (1490013)Instructions burned: 150 (million)
% 42.13/8.79 % (1490015)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2860340980:i=14155:bd=all_2945 on theBenchmark for (2945ds/14155Mi)
% 42.13/8.79 % (1490010)Instruction limit reached!
% 42.13/8.79 % (1490010)------------------------------
% 42.13/8.79 % (1490010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490010)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490010)Termination reason: Instruction limit
% 42.13/8.79 % (1490010)Termination phase: Function definition elimination
% 42.13/8.79 % (1490010)Time elapsed: 2.162 s
% 42.13/8.79 % (1490010)Peak memory usage: 245 MB
% 42.13/8.79 % (1490010)Instructions burned: 6063 (million)
% 42.13/8.79 % (1490017)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3685411931:i=667:av=off:fsr=off_2931 on theBenchmark for (2931ds/667Mi)
% 42.13/8.79 % (1489993)Instruction limit reached!
% 42.13/8.79 % (1489993)------------------------------
% 42.13/8.79 % (1489993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1489993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1489993)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1489993)Termination reason: Instruction limit
% 42.13/8.79 % (1489993)Termination phase: Saturation
% 42.13/8.79 % (1489993)Time elapsed: 3.918 s
% 42.13/8.79 % (1489993)Peak memory usage: 621 MB
% 42.13/8.79 % (1489993)Instructions burned: 5202 (million)
% 42.13/8.79 % (1490017)Instruction limit reached!
% 42.13/8.79 % (1490017)------------------------------
% 42.13/8.79 % (1490017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490017)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490017)Termination reason: Instruction limit
% 42.13/8.79 % (1490017)Termination phase: NewCNF
% 42.13/8.79 % (1490017)Time elapsed: 0.338 s
% 42.13/8.79 % (1490017)Peak memory usage: 186 MB
% 42.13/8.79 % (1490017)Instructions burned: 669 (million)
% 42.13/8.79 % (1490019)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=4236739953:s2a=on:i=185:s2at=1.8:fdi=4_2927 on theBenchmark for (2927ds/185Mi)
% 42.13/8.79 % (1490020)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3447793163:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2926 on theBenchmark for (2926ds/193Mi)
% 42.13/8.79 % (1490001)First to succeed.
% 42.13/8.79 % (1490001)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1489954"
% 42.13/8.79 % (1490019)Instruction limit reached!
% 42.13/8.79 % (1490019)------------------------------
% 42.13/8.79 % (1490019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490019)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490019)Termination reason: Instruction limit
% 42.13/8.79 % (1490019)Termination phase: SInE selection
% 42.13/8.79 % (1490019)Time elapsed: 0.133 s
% 42.13/8.79 % (1490019)Peak memory usage: 136 MB
% 42.13/8.79 % (1490019)Instructions burned: 186 (million)
% 42.13/8.79 % (1490020)Instruction limit reached!
% 42.13/8.79 % (1490020)------------------------------
% 42.13/8.79 % (1490020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.13/8.79 % (1490020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.13/8.79 % (1490020)CaDiCaL version: 2.1.3
% 42.13/8.79 % (1490020)Termination reason: Instruction limit
% 42.13/8.79 % (1490020)Termination phase: SInE selection
% 42.13/8.79 % (1490020)Time elapsed: 0.090 s
% 42.13/8.79 % (1490020)Peak memory usage: 137 MB
% 42.13/8.79 % (1490020)Instructions burned: 195 (million)
% 42.13/8.79 % (1490023)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1925921614:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2924 on theBenchmark for (2924ds/4850Mi)
% 42.13/8.79 % (1490024)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=191159014:i=12111:sd=1:ss=included_2924 on theBenchmark for (2924ds/12111Mi)
% 42.13/8.79 % (1490001)Refutation found. Thanks to Tanya!
% 42.13/8.79 % SZS status Theorem for theBenchmark
% 42.13/8.79 % SZS output start Proof for theBenchmark
% See solution above
% 43.14/8.92 % (1490001)------------------------------
% 43.14/8.92 % (1490001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.14/8.92 % (1490001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.14/8.92 % (1490001)CaDiCaL version: 2.1.3
% 43.14/8.92 % (1490001)Termination reason: Refutation
% 43.14/8.92 % (1490001)Time elapsed: 3.599 s
% 43.14/8.92 % (1490001)Peak memory usage: 285 MB
% 43.14/8.92 % (1490001)Instructions burned: 5920 (million)
% 43.14/8.92 % (1490001)------------------------------
% 43.14/8.92 % (1490001)------------------------------
% 43.14/8.92 % (1489954)Success in time 7.921 s
% 43.14/8.92 % Vampire exiting
%------------------------------------------------------------------------------