%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT303+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:48:18 AM UTC 2026
% Result : Theorem 0.14s 0.49s
% Output : Refutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 23
% Syntax : Number of formulae : 164 ( 27 unt; 9 def)
% Number of atoms : 567 ( 17 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 662 ( 259 ~; 277 |; 87 &)
% ( 17 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 9 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 96 ( 0 sgn 92 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(X0),X1),X0)
=> v13_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t27_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(X0),X1),X0)
=> v13_lattices(X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f14,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f16,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f21,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_filter_2) ).
fof(f25,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f26,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f48,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f49,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f60,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f78,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> k6_domain_1(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_domain_1) ).
fof(f79,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(f82,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
=> v14_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t14_filter_0) ).
fof(f84,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f89,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_lattice2) ).
fof(f106,plain,
? [X0] :
( ? [X1] :
( ~ v13_lattices(X0)
& m2_filter_2(k6_domain_1(u1_struct_0(X0),X1),X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f107,plain,
? [X0] :
( ? [X1] :
( ~ v13_lattices(X0)
& m2_filter_2(k6_domain_1(u1_struct_0(X0),X1),X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f106]) ).
fof(f125,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f126,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f125]) ).
fof(f129,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f130,plain,
! [X0,X1] :
( m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f21]) ).
fof(f131,plain,
! [X0,X1] :
( m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f130]) ).
fof(f135,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f136,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f156,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f157,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f156]) ).
fof(f158,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f49]) ).
fof(f159,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f158]) ).
fof(f172,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,[],[f60]) ).
fof(f173,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,[],[f172]) ).
fof(f181,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f78]) ).
fof(f182,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f181]) ).
fof(f183,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,[],[f79]) ).
fof(f184,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,[],[f183]) ).
fof(f185,plain,
! [X0] :
( ! [X1] :
( v14_lattices(X0)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f82]) ).
fof(f186,plain,
! [X0] :
( ! [X1] :
( v14_lattices(X0)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f185]) ).
fof(f188,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f84]) ).
fof(f189,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f188]) ).
fof(f196,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f89]) ).
fof(f197,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f196]) ).
fof(f201,definition,
! [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)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f202,plain,
! [X0] :
( sP0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f173,f201]) ).
fof(f203,plain,
( ~ v13_lattices(sK1)
& m2_filter_2(k6_domain_1(u1_struct_0(sK1),sK2),sK1)
& m1_subset_1(sK2,u1_struct_0(sK1))
& ~ v3_struct_0(sK1)
& v10_lattices(sK1)
& l3_lattices(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(X1,sK2)],[f107]) ).
fof(f215,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)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f201]) ).
fof(f232,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,[],[f184]) ).
fof(f234,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f189]) ).
fof(f235,plain,
! [X0] :
( ( ( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0)) )
& ( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f197]) ).
fof(f236,plain,
l3_lattices(sK1),
inference(cnf_transformation,[],[f203]) ).
fof(f237,plain,
v10_lattices(sK1),
inference(cnf_transformation,[],[f203]) ).
fof(f238,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f203]) ).
fof(f239,plain,
m1_subset_1(sK2,u1_struct_0(sK1)),
inference(cnf_transformation,[],[f203]) ).
fof(f240,plain,
m2_filter_2(k6_domain_1(u1_struct_0(sK1),sK2),sK1),
inference(cnf_transformation,[],[f203]) ).
fof(f241,plain,
~ v13_lattices(sK1),
inference(cnf_transformation,[],[f203]) ).
fof(f264,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f267,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f269,plain,
! [X0,X1] :
( m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f131]) ).
fof(f272,plain,
! [X0] :
( ~ l2_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f135]) ).
fof(f273,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f301,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f302,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f159]) ).
fof(f323,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f215]) ).
fof(f332,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f202]) ).
fof(f387,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0)
| k6_domain_1(X0,X1) = k1_tarski(X1) ),
inference(cnf_transformation,[],[f182]) ).
fof(f388,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,[],[f232]) ).
fof(f393,plain,
! [X0,X1] :
( ~ m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
| v14_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f186]) ).
fof(f395,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f234]) ).
fof(f402,plain,
! [X0] :
( ~ v14_lattices(k1_lattice2(X0))
| v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f235]) ).
fof(f416,plain,
l2_lattices(sK1),
inference(resolution,[],[f273,f236]) ).
fof(f422,plain,
l1_struct_0(sK1),
inference(resolution,[],[f416,f272]) ).
fof(f634,plain,
( v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| sP0(sK1) ),
inference(resolution,[],[f332,f236]) ).
fof(f642,plain,
( ~ v10_lattices(sK1)
| sP0(sK1) ),
inference(forward_subsumption_resolution,[],[f634,f238]) ).
fof(f645,plain,
sP0(sK1),
inference(forward_subsumption_resolution,[],[f642,f237]) ).
fof(f656,definition,
( spl30_24
<=> v1_xboole_0(u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl30_24])],[avatar_definition]) ).
fof(f657,plain,
( ~ v1_xboole_0(u1_struct_0(sK1))
| spl30_24 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f658,plain,
( v1_xboole_0(u1_struct_0(sK1))
| ~ spl30_24 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f665,plain,
( v3_struct_0(sK1)
| ~ l1_struct_0(sK1)
| ~ spl30_24 ),
inference(resolution,[],[f658,f302]) ).
fof(f670,plain,
( ~ l1_struct_0(sK1)
| ~ spl30_24 ),
inference(forward_subsumption_resolution,[],[f665,f238]) ).
fof(f671,plain,
( $false
| ~ spl30_24 ),
inference(forward_subsumption_resolution,[],[f670,f422]) ).
fof(f672,plain,
~ spl30_24,
inference(avatar_contradiction_clause,[],[f671]) ).
fof(f752,plain,
( v1_xboole_0(u1_struct_0(sK1))
| k6_domain_1(u1_struct_0(sK1),sK2) = k1_tarski(sK2) ),
inference(resolution,[],[f387,f239]) ).
fof(f760,plain,
( k6_domain_1(u1_struct_0(sK1),sK2) = k1_tarski(sK2)
| spl30_24 ),
inference(forward_subsumption_resolution,[],[f752,f657]) ).
fof(f767,plain,
( m2_filter_2(k1_tarski(sK2),sK1)
| spl30_24 ),
inference(superposition,[],[f240,f760]) ).
fof(f835,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(resolution,[],[f395,f388]) ).
fof(f839,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(forward_subsumption_resolution,[],[f835,f301]) ).
fof(f841,plain,
! [X0,X1] :
( m1_filter_0(X0,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_filter_2(X0,X1)
| ~ v10_lattices(k1_lattice2(X1)) ),
inference(forward_subsumption_resolution,[],[f839,f267]) ).
fof(f871,plain,
( sK2 = k5_filter_2(sK1,sK2)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolution,[],[f264,f239]) ).
fof(f873,plain,
( sK2 = k5_filter_2(sK1,sK2)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f871,f238]) ).
fof(f874,plain,
( sK2 = k5_filter_2(sK1,sK2)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f873,f237]) ).
fof(f875,plain,
sK2 = k5_filter_2(sK1,sK2),
inference(forward_subsumption_resolution,[],[f874,f236]) ).
fof(f888,plain,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(superposition,[],[f269,f875]) ).
fof(f889,plain,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f888,f238]) ).
fof(f891,plain,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f889,f237]) ).
fof(f893,plain,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f891,f236]) ).
fof(f894,plain,
m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1))),
inference(forward_subsumption_resolution,[],[f893,f239]) ).
fof(f896,plain,
( v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| k1_tarski(sK2) = k6_domain_1(u1_struct_0(k1_lattice2(sK1)),sK2) ),
inference(resolution,[],[f894,f387]) ).
fof(f899,definition,
( spl30_28
<=> v1_xboole_0(u1_struct_0(k1_lattice2(sK1))) ),
introduced(definition,[new_symbols(definition,[spl30_28])],[avatar_definition]) ).
fof(f901,plain,
( v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| ~ spl30_28 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f908,definition,
( spl30_30
<=> k1_tarski(sK2) = k6_domain_1(u1_struct_0(k1_lattice2(sK1)),sK2) ),
introduced(definition,[new_symbols(definition,[spl30_30])],[avatar_definition]) ).
fof(f910,plain,
( k1_tarski(sK2) = k6_domain_1(u1_struct_0(k1_lattice2(sK1)),sK2)
| ~ spl30_30 ),
inference(avatar_component_clause,[],[f908]) ).
fof(f911,plain,
( spl30_30
| spl30_28 ),
inference(avatar_split_clause,[],[f896,f899,f908]) ).
fof(f913,definition,
( spl30_31
<=> l3_lattices(k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl30_31])],[avatar_definition]) ).
fof(f914,plain,
( l3_lattices(k1_lattice2(sK1))
| ~ spl30_31 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f915,plain,
( ~ l3_lattices(k1_lattice2(sK1))
| spl30_31 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f917,definition,
( spl30_32
<=> v10_lattices(k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl30_32])],[avatar_definition]) ).
fof(f918,plain,
( v10_lattices(k1_lattice2(sK1))
| ~ spl30_32 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f919,plain,
( ~ v10_lattices(k1_lattice2(sK1))
| spl30_32 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f921,definition,
( spl30_33
<=> v3_struct_0(k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl30_33])],[avatar_definition]) ).
fof(f922,plain,
( ~ v3_struct_0(k1_lattice2(sK1))
| spl30_33 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f923,plain,
( v3_struct_0(k1_lattice2(sK1))
| ~ spl30_33 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f933,plain,
( ~ sP0(sK1)
| spl30_32 ),
inference(resolution,[],[f919,f323]) ).
fof(f934,plain,
( $false
| spl30_32 ),
inference(forward_subsumption_resolution,[],[f933,f645]) ).
fof(f935,plain,
spl30_32,
inference(avatar_contradiction_clause,[],[f934]) ).
fof(f950,plain,
( ~ l3_lattices(sK1)
| spl30_31 ),
inference(resolution,[],[f915,f267]) ).
fof(f951,plain,
( $false
| spl30_31 ),
inference(forward_subsumption_resolution,[],[f950,f236]) ).
fof(f952,plain,
spl30_31,
inference(avatar_contradiction_clause,[],[f951]) ).
fof(f962,plain,
( l2_lattices(k1_lattice2(sK1))
| ~ spl30_31 ),
inference(resolution,[],[f914,f273]) ).
fof(f1002,plain,
( v3_struct_0(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_33 ),
inference(resolution,[],[f923,f301]) ).
fof(f1006,plain,
( ~ l3_lattices(sK1)
| ~ spl30_33 ),
inference(forward_subsumption_resolution,[],[f1002,f238]) ).
fof(f1007,plain,
( $false
| ~ spl30_33 ),
inference(forward_subsumption_resolution,[],[f1006,f236]) ).
fof(f1008,plain,
~ spl30_33,
inference(avatar_contradiction_clause,[],[f1007]) ).
fof(f1042,plain,
( l1_struct_0(k1_lattice2(sK1))
| ~ spl30_31 ),
inference(resolution,[],[f962,f272]) ).
fof(f1086,plain,
( v3_struct_0(k1_lattice2(sK1))
| ~ l1_struct_0(k1_lattice2(sK1))
| ~ spl30_28 ),
inference(resolution,[],[f901,f302]) ).
fof(f1091,plain,
( ~ l1_struct_0(k1_lattice2(sK1))
| ~ spl30_28
| spl30_33 ),
inference(forward_subsumption_resolution,[],[f1086,f922]) ).
fof(f1092,plain,
( $false
| ~ spl30_28
| ~ spl30_31
| spl30_33 ),
inference(forward_subsumption_resolution,[],[f1091,f1042]) ).
fof(f1093,plain,
( ~ spl30_28
| ~ spl30_31
| spl30_33 ),
inference(avatar_contradiction_clause,[],[f1092]) ).
fof(f1953,plain,
( ~ m1_filter_0(k1_tarski(sK2),k1_lattice2(sK1))
| v14_lattices(k1_lattice2(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ spl30_30 ),
inference(superposition,[],[f393,f910]) ).
fof(f1960,plain,
( ~ m1_filter_0(k1_tarski(sK2),k1_lattice2(sK1))
| v14_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ spl30_30 ),
inference(forward_subsumption_resolution,[],[f1953,f894]) ).
fof(f1964,plain,
( ~ m1_filter_0(k1_tarski(sK2),k1_lattice2(sK1))
| v14_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ spl30_30
| spl30_33 ),
inference(forward_subsumption_resolution,[],[f1960,f922]) ).
fof(f1965,plain,
( ~ m1_filter_0(k1_tarski(sK2),k1_lattice2(sK1))
| v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ spl30_30
| ~ spl30_32
| spl30_33 ),
inference(forward_subsumption_resolution,[],[f1964,f918]) ).
fof(f1966,plain,
( ~ m1_filter_0(k1_tarski(sK2),k1_lattice2(sK1))
| v14_lattices(k1_lattice2(sK1))
| ~ spl30_30
| ~ spl30_31
| ~ spl30_32
| spl30_33 ),
inference(forward_subsumption_resolution,[],[f1965,f914]) ).
fof(f1968,definition,
( spl30_146
<=> v14_lattices(k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl30_146])],[avatar_definition]) ).
fof(f1970,plain,
( v14_lattices(k1_lattice2(sK1))
| ~ spl30_146 ),
inference(avatar_component_clause,[],[f1968]) ).
fof(f1972,definition,
( spl30_147
<=> m1_filter_0(k1_tarski(sK2),k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl30_147])],[avatar_definition]) ).
fof(f1974,plain,
( ~ m1_filter_0(k1_tarski(sK2),k1_lattice2(sK1))
| spl30_147 ),
inference(avatar_component_clause,[],[f1972]) ).
fof(f1975,plain,
( spl30_146
| ~ spl30_147
| ~ spl30_30
| ~ spl30_31
| ~ spl30_32
| spl30_33 ),
inference(avatar_split_clause,[],[f1966,f921,f917,f913,f908,f1972,f1968]) ).
fof(f1988,plain,
( v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_filter_2(k1_tarski(sK2),sK1)
| ~ v10_lattices(k1_lattice2(sK1))
| spl30_147 ),
inference(resolution,[],[f1974,f841]) ).
fof(f1989,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_filter_2(k1_tarski(sK2),sK1)
| ~ v10_lattices(k1_lattice2(sK1))
| spl30_147 ),
inference(forward_subsumption_resolution,[],[f1988,f238]) ).
fof(f1990,plain,
( ~ l3_lattices(sK1)
| ~ m2_filter_2(k1_tarski(sK2),sK1)
| ~ v10_lattices(k1_lattice2(sK1))
| spl30_147 ),
inference(forward_subsumption_resolution,[],[f1989,f237]) ).
fof(f1991,plain,
( ~ m2_filter_2(k1_tarski(sK2),sK1)
| ~ v10_lattices(k1_lattice2(sK1))
| spl30_147 ),
inference(forward_subsumption_resolution,[],[f1990,f236]) ).
fof(f1992,plain,
( ~ v10_lattices(k1_lattice2(sK1))
| spl30_24
| spl30_147 ),
inference(forward_subsumption_resolution,[],[f1991,f767]) ).
fof(f1993,plain,
( $false
| spl30_24
| ~ spl30_32
| spl30_147 ),
inference(forward_subsumption_resolution,[],[f1992,f918]) ).
fof(f1994,plain,
( spl30_24
| ~ spl30_32
| spl30_147 ),
inference(avatar_contradiction_clause,[],[f1993]) ).
fof(f2003,plain,
( v13_lattices(sK1)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_146 ),
inference(resolution,[],[f1970,f402]) ).
fof(f2006,plain,
( v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_146 ),
inference(forward_subsumption_resolution,[],[f2003,f241]) ).
fof(f2008,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_146 ),
inference(forward_subsumption_resolution,[],[f2006,f238]) ).
fof(f2018,plain,
( ~ l3_lattices(sK1)
| ~ spl30_146 ),
inference(forward_subsumption_resolution,[],[f2008,f237]) ).
fof(f2019,plain,
( $false
| ~ spl30_146 ),
inference(forward_subsumption_resolution,[],[f2018,f236]) ).
fof(f2020,plain,
~ spl30_146,
inference(avatar_contradiction_clause,[],[f2019]) ).
cnf(s20,plain,
~ spl30_24,
inference(sat_conversion,[],[f672]) ).
cnf(s28,plain,
( spl30_28
| spl30_30 ),
inference(sat_conversion,[],[f911]) ).
cnf(s30,plain,
spl30_32,
inference(sat_conversion,[],[f935]) ).
cnf(s32,plain,
spl30_31,
inference(sat_conversion,[],[f952]) ).
cnf(s41,plain,
~ spl30_33,
inference(sat_conversion,[],[f1008]) ).
cnf(s45,plain,
( ~ spl30_28
| ~ spl30_31
| spl30_33 ),
inference(sat_conversion,[],[f1093]) ).
cnf(s115,plain,
( ~ spl30_30
| ~ spl30_31
| ~ spl30_32
| spl30_33
| spl30_146
| ~ spl30_147 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s116,plain,
( spl30_24
| ~ spl30_32
| spl30_147 ),
inference(sat_conversion,[],[f1994]) ).
cnf(s118,plain,
~ spl30_146,
inference(sat_conversion,[],[f2020]) ).
cnf(s119,plain,
( ~ spl30_30
| ~ spl30_31
| ~ spl30_32
| spl30_33
| ~ spl30_147 ),
inference(rat,[],[s115,s118]) ).
cnf(s129,plain,
~ spl30_28,
inference(rat,[],[s45,s41,s32]) ).
cnf(s164,plain,
spl30_30,
inference(rat,[],[s28,s129]) ).
cnf(s165,plain,
~ spl30_147,
inference(rat,[],[s119,s30,s41,s32,s164]) ).
cnf(s166,plain,
spl30_24,
inference(rat,[],[s116,s30,s165]) ).
cnf(s169,plain,
$false,
inference(rat,[],[s20,s166]) ).
fof(f2021,plain,
$false,
inference(avatar_sat_refutation,[],[s169]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT303+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 14:30:01 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.49 % (3624821)Will run a generic schedule for satisfiability detection.
% 0.14/0.49 % (3624828)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1689850594:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.14/0.49 % (3624827)% WARNING: option uhcvi not known.
% 0.14/0.49 % (3624826)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1078108251_2999 on theBenchmark for (2999ds/0Mi)
% 0.14/0.49 % (3624827)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=755385861:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.14/0.49 % (3624829)dis+10_1_sil=32000:sp=arity:random_seed=3347627125:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.14/0.49 % (3624830)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3966882621:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.14/0.49 % (3624831)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1569720889:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.14/0.49 % (3624832)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3846538178:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.14/0.49 % TRYING [1]
% 0.14/0.49 % TRYING [2]
% 0.14/0.49 % TRYING [3]
% 0.14/0.49 % TRYING [4]
% 0.14/0.49 % (3624829) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3624821-3624829"...
% 0.14/0.49 % (3624829)...printing done.
% 0.14/0.49 % (3624829)Refutation found. Thanks to Tanya!
% 0.14/0.49 % SZS status Theorem for theBenchmark
% 0.14/0.49 % SZS output start Proof for theBenchmark
% See solution above
% 0.14/0.49 % (3624829)------------------------------
% 0.14/0.49 % (3624829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.14/0.49 % (3624829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.14/0.49 % (3624829)CaDiCaL version: 2.1.3
% 0.14/0.49 % (3624829)Termination reason: Refutation
% 0.14/0.49 % (3624829)Time elapsed: 0.038 s
% 0.14/0.49 % (3624829)Peak memory usage: 13 MB
% 0.14/0.49 % (3624829)Instructions burned: 55 (million)
% 0.14/0.49 % (3624821)Success in time 0.078 s
% 0.14/0.49 % Vampire exiting
%------------------------------------------------------------------------------