%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT337+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:29 AM UTC 2026
% Result : Theorem 0.23s 0.56s
% Output : Refutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 20
% Syntax : Number of formulae : 207 ( 31 unt; 12 def)
% Number of atoms : 974 ( 0 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 1172 ( 405 ~; 588 |; 144 &)
% ( 12 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 34 ( 33 usr; 13 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 103 ( 0 sgn 97 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0)
& r3_lattices(X0,X1,X2) )
=> ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t87_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))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0)
& r3_lattices(X0,X1,X2) )
=> ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f12,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc5_lattices) ).
fof(f13,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v17_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc6_lattices) ).
fof(f14,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& v10_lattices(X0)
& v12_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc7_lattices) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f50,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_filter_2) ).
fof(f81,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( v11_lattices(X0)
=> v11_lattices(k23_filter_2(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t78_filter_2) ).
fof(f83,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0)
& v12_lattices(X0)
& r3_lattices(X0,X1,X2) )
=> ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t86_filter_2) ).
fof(f97,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0)
& r3_lattices(X0,X1,X2)
& m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f98,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0)
& r3_lattices(X0,X1,X2)
& m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f97]) ).
fof(f114,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f115,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f117,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f116]) ).
fof(f118,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& v10_lattices(X0)
& v12_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f119,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& v10_lattices(X0)
& v12_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f118]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f122]) ).
fof(f152,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f153,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(flattening,[],[f152]) ).
fof(f177,plain,
! [X0] :
( ! [X1] :
( v11_lattices(k23_filter_2(X0,X1))
| ~ v11_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f81]) ).
fof(f178,plain,
! [X0] :
( ! [X1] :
( v11_lattices(k23_filter_2(X0,X1))
| ~ v11_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f177]) ).
fof(f180,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f181,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f180]) ).
fof(f183,plain,
( ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(cnf_transformation,[],[f98]) ).
fof(f184,plain,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f98]) ).
fof(f185,plain,
r3_lattices(sK0,sK1,sK2),
inference(cnf_transformation,[],[f98]) ).
fof(f186,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f98]) ).
fof(f187,plain,
v17_lattices(sK0),
inference(cnf_transformation,[],[f98]) ).
fof(f189,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f98]) ).
fof(f190,plain,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f98]) ).
fof(f192,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f98]) ).
fof(f208,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v16_lattices(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f209,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v15_lattices(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f212,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v11_lattices(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f213,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v11_lattices(X0)
| v3_struct_0(X0)
| v17_lattices(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f214,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v11_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v12_lattices(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f223,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_lattice4(k22_filter_2(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f224,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(k22_filter_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f265,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k23_filter_2(X0,X1)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f273,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ v3_struct_0(k23_filter_2(X0,X1)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f393,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ v11_lattices(X0)
| v11_lattices(k23_filter_2(X0,X1)) ),
inference(cnf_transformation,[],[f178]) ).
fof(f395,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f181]) ).
fof(f396,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f181]) ).
fof(f397,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f181]) ).
fof(f401,plain,
~ v10_lattices(sK0),
inference(consistent_polarity_flipping,[],[f192]) ).
fof(f402,plain,
~ m1_subset_1(sK1,u1_struct_0(sK0)),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f404,plain,
~ v17_lattices(sK0),
inference(consistent_polarity_flipping,[],[f187]) ).
fof(f405,plain,
~ m1_subset_1(sK2,u1_struct_0(sK0)),
inference(consistent_polarity_flipping,[],[f184]) ).
fof(f406,plain,
( ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f417,plain,
! [X0] :
( ~ v11_lattices(X0)
| v17_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f420,plain,
! [X0] :
( v17_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| v15_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f421,plain,
! [X0] :
( ~ v16_lattices(X0)
| v17_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f422,plain,
! [X0] :
( ~ v17_lattices(X0)
| v16_lattices(X0)
| ~ v15_lattices(X0)
| v11_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f429,plain,
! [X0] :
( ~ v12_lattices(X0)
| v11_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f432,plain,
! [X2,X0,X1] :
( v1_xboole_0(k22_filter_2(X0,X1,X2))
| m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(X2,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f224]) ).
fof(f433,plain,
! [X2,X0,X1] :
( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
| m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(X2,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f223]) ).
fof(f472,plain,
! [X0,X1] :
( ~ v3_struct_0(k23_filter_2(X0,X1))
| ~ v1_xboole_0(X1)
| ~ l3_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_lattice4(X1,X0) ),
inference(consistent_polarity_flipping,[],[f273]) ).
fof(f480,plain,
! [X0,X1] :
( ~ v10_lattices(k23_filter_2(X0,X1))
| ~ v1_xboole_0(X1)
| ~ l3_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_lattice4(X1,X0) ),
inference(consistent_polarity_flipping,[],[f265]) ).
fof(f554,plain,
! [X0,X1] :
( ~ v11_lattices(k23_filter_2(X0,X1))
| v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_lattice4(X1,X0)
| ~ v1_xboole_0(X1)
| v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f393]) ).
fof(f558,plain,
! [X2,X0,X1] :
( v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| m1_subset_1(X2,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| v12_lattices(X0)
| ~ l3_lattices(X0)
| v16_lattices(X0)
| ~ v15_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f397]) ).
fof(f559,plain,
! [X2,X0,X1] :
( ~ v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| m1_subset_1(X2,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| v12_lattices(X0)
| ~ l3_lattices(X0)
| v16_lattices(X0)
| ~ v15_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f396]) ).
fof(f560,plain,
! [X2,X0,X1] :
( l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| m1_subset_1(X2,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| v12_lattices(X0)
| ~ l3_lattices(X0)
| v16_lattices(X0)
| ~ v15_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f395]) ).
fof(f563,definition,
( spl30_1
<=> v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
fof(f565,plain,
( v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_1 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f567,definition,
( spl30_2
<=> v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition]) ).
fof(f569,plain,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_2 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f571,definition,
( spl30_3
<=> v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition]) ).
fof(f573,plain,
( v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_3 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl30_4
<=> l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition]) ).
fof(f576,plain,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_4 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f577,plain,
( ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| spl30_4 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f578,plain,
( spl30_1
| spl30_2
| spl30_3
| ~ spl30_4 ),
inference(avatar_split_clause,[],[f406,f575,f571,f567,f563]) ).
fof(f614,plain,
( ~ l3_lattices(sK0)
| v3_struct_0(sK0)
| v15_lattices(sK0) ),
inference(resolution,[],[f420,f404]) ).
fof(f616,plain,
( v3_struct_0(sK0)
| v15_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f614,f186]) ).
fof(f617,plain,
v15_lattices(sK0),
inference(forward_subsumption_resolution,[],[f616,f189]) ).
fof(f779,plain,
( m1_subset_1(sK2,u1_struct_0(sK0))
| ~ r3_lattices(sK0,sK1,sK2)
| v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_4 ),
inference(resolution,[],[f560,f577]) ).
fof(f780,plain,
( ~ r3_lattices(sK0,sK1,sK2)
| v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_4 ),
inference(forward_subsumption_resolution,[],[f779,f405]) ).
fof(f781,plain,
( v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_4 ),
inference(forward_subsumption_resolution,[],[f780,f185]) ).
fof(f782,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_4 ),
inference(forward_subsumption_resolution,[],[f781,f186]) ).
fof(f783,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_4 ),
inference(forward_subsumption_resolution,[],[f782,f617]) ).
fof(f784,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_4 ),
inference(forward_subsumption_resolution,[],[f783,f401]) ).
fof(f785,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_4 ),
inference(forward_subsumption_resolution,[],[f784,f189]) ).
fof(f786,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| spl30_4 ),
inference(forward_subsumption_resolution,[],[f785,f402]) ).
fof(f788,definition,
( spl30_15
<=> v16_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl30_15])],[avatar_definition]) ).
fof(f789,plain,
( ~ v16_lattices(sK0)
| spl30_15 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f790,plain,
( v16_lattices(sK0)
| ~ spl30_15 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f792,definition,
( spl30_16
<=> v12_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl30_16])],[avatar_definition]) ).
fof(f793,plain,
( ~ v12_lattices(sK0)
| spl30_16 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f794,plain,
( v12_lattices(sK0)
| ~ spl30_16 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f795,plain,
( spl30_15
| spl30_16
| spl30_4 ),
inference(avatar_split_clause,[],[f786,f575,f792,f788]) ).
fof(f798,definition,
( spl30_17
<=> v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl30_17])],[avatar_definition]) ).
fof(f800,plain,
( v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_17 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f802,definition,
( spl30_18
<=> v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl30_18])],[avatar_definition]) ).
fof(f803,plain,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_18 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f804,plain,
( ~ v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| spl30_18 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f806,definition,
( spl30_19
<=> v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl30_19])],[avatar_definition]) ).
fof(f808,plain,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_19 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f810,plain,
( m1_subset_1(sK2,u1_struct_0(sK0))
| ~ r3_lattices(sK0,sK1,sK2)
| v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_18 ),
inference(resolution,[],[f804,f558]) ).
fof(f811,plain,
( ~ r3_lattices(sK0,sK1,sK2)
| v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_18 ),
inference(forward_subsumption_resolution,[],[f810,f405]) ).
fof(f812,plain,
( v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_18 ),
inference(forward_subsumption_resolution,[],[f811,f185]) ).
fof(f813,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_18 ),
inference(forward_subsumption_resolution,[],[f812,f186]) ).
fof(f814,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_18 ),
inference(forward_subsumption_resolution,[],[f813,f617]) ).
fof(f815,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_18 ),
inference(forward_subsumption_resolution,[],[f814,f401]) ).
fof(f816,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_18 ),
inference(forward_subsumption_resolution,[],[f815,f189]) ).
fof(f817,plain,
( v12_lattices(sK0)
| v16_lattices(sK0)
| spl30_18 ),
inference(forward_subsumption_resolution,[],[f816,f402]) ).
fof(f818,plain,
( spl30_15
| spl30_16
| spl30_18 ),
inference(avatar_split_clause,[],[f817,f802,f792,f788]) ).
fof(f819,plain,
( v17_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_15 ),
inference(resolution,[],[f790,f421]) ).
fof(f820,plain,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_15 ),
inference(forward_subsumption_resolution,[],[f819,f404]) ).
fof(f821,plain,
( ~ l3_lattices(sK0)
| ~ spl30_15 ),
inference(forward_subsumption_resolution,[],[f820,f189]) ).
fof(f822,plain,
( $false
| ~ spl30_15 ),
inference(forward_subsumption_resolution,[],[f821,f186]) ).
fof(f823,plain,
~ spl30_15,
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f835,plain,
( v11_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_16 ),
inference(resolution,[],[f794,f429]) ).
fof(f836,plain,
( v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_16 ),
inference(forward_subsumption_resolution,[],[f835,f401]) ).
fof(f837,plain,
( v11_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_16 ),
inference(forward_subsumption_resolution,[],[f836,f189]) ).
fof(f838,plain,
( v11_lattices(sK0)
| ~ spl30_16 ),
inference(forward_subsumption_resolution,[],[f837,f186]) ).
fof(f839,plain,
( v17_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_16 ),
inference(resolution,[],[f838,f417]) ).
fof(f840,plain,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_16 ),
inference(forward_subsumption_resolution,[],[f839,f404]) ).
fof(f841,plain,
( ~ l3_lattices(sK0)
| ~ spl30_16 ),
inference(forward_subsumption_resolution,[],[f840,f189]) ).
fof(f842,plain,
( $false
| ~ spl30_16 ),
inference(forward_subsumption_resolution,[],[f841,f186]) ).
fof(f843,plain,
~ spl30_16,
inference(avatar_contradiction_clause,[],[f842]) ).
fof(f887,plain,
( v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| v11_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_17 ),
inference(resolution,[],[f800,f554]) ).
fof(f889,plain,
( v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| v11_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_17 ),
inference(forward_subsumption_resolution,[],[f887,f401]) ).
fof(f890,plain,
( ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| v11_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_17 ),
inference(forward_subsumption_resolution,[],[f889,f189]) ).
fof(f891,plain,
( ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| v11_lattices(sK0)
| ~ spl30_17 ),
inference(forward_subsumption_resolution,[],[f890,f186]) ).
fof(f893,definition,
( spl30_28
<=> v11_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl30_28])],[avatar_definition]) ).
fof(f895,plain,
( v11_lattices(sK0)
| ~ spl30_28 ),
inference(avatar_component_clause,[],[f893]) ).
fof(f897,definition,
( spl30_29
<=> v1_xboole_0(k22_filter_2(sK0,sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl30_29])],[avatar_definition]) ).
fof(f898,plain,
( v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| ~ spl30_29 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f899,plain,
( ~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| spl30_29 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f901,definition,
( spl30_30
<=> m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0) ),
introduced(definition,[new_symbols(definition,[spl30_30])],[avatar_definition]) ).
fof(f902,plain,
( m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_30 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f903,plain,
( ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| spl30_30 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f917,plain,
( m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_29 ),
inference(resolution,[],[f899,f432]) ).
fof(f923,plain,
( ~ l3_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_29 ),
inference(forward_subsumption_resolution,[],[f917,f402]) ).
fof(f924,plain,
( v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_29 ),
inference(forward_subsumption_resolution,[],[f923,f186]) ).
fof(f925,plain,
( v3_struct_0(sK0)
| m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_29 ),
inference(forward_subsumption_resolution,[],[f924,f401]) ).
fof(f926,plain,
( m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_29 ),
inference(forward_subsumption_resolution,[],[f925,f189]) ).
fof(f927,plain,
( $false
| spl30_29 ),
inference(forward_subsumption_resolution,[],[f926,f405]) ).
fof(f928,plain,
spl30_29,
inference(avatar_contradiction_clause,[],[f927]) ).
fof(f940,plain,
( m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_30 ),
inference(resolution,[],[f903,f433]) ).
fof(f941,plain,
( ~ l3_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_30 ),
inference(forward_subsumption_resolution,[],[f940,f402]) ).
fof(f942,plain,
( v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_30 ),
inference(forward_subsumption_resolution,[],[f941,f186]) ).
fof(f943,plain,
( v3_struct_0(sK0)
| m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_30 ),
inference(forward_subsumption_resolution,[],[f942,f401]) ).
fof(f944,plain,
( m1_subset_1(sK2,u1_struct_0(sK0))
| spl30_30 ),
inference(forward_subsumption_resolution,[],[f943,f189]) ).
fof(f945,plain,
( $false
| spl30_30 ),
inference(forward_subsumption_resolution,[],[f944,f405]) ).
fof(f946,plain,
spl30_30,
inference(avatar_contradiction_clause,[],[f945]) ).
fof(f948,plain,
( ~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| ~ l3_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_2 ),
inference(resolution,[],[f569,f480]) ).
fof(f952,plain,
( ~ l3_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_2
| ~ spl30_29 ),
inference(forward_subsumption_resolution,[],[f948,f898]) ).
fof(f979,plain,
( v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_2
| ~ spl30_29 ),
inference(forward_subsumption_resolution,[],[f952,f186]) ).
fof(f981,plain,
( v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_2
| ~ spl30_29 ),
inference(forward_subsumption_resolution,[],[f979,f401]) ).
fof(f983,plain,
( ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_2
| ~ spl30_29 ),
inference(forward_subsumption_resolution,[],[f981,f189]) ).
fof(f985,plain,
( ~ spl30_30
| ~ spl30_2
| ~ spl30_29 ),
inference(avatar_split_clause,[],[f983,f897,f567,f901]) ).
fof(f995,plain,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_3 ),
inference(resolution,[],[f573,f422]) ).
fof(f996,plain,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_3
| ~ spl30_18 ),
inference(forward_subsumption_resolution,[],[f995,f803]) ).
fof(f997,plain,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ spl30_3
| ~ spl30_4
| ~ spl30_18 ),
inference(forward_subsumption_resolution,[],[f996,f576]) ).
fof(f998,plain,
( spl30_1
| spl30_17
| spl30_19
| ~ spl30_3
| ~ spl30_4
| ~ spl30_18 ),
inference(avatar_split_clause,[],[f997,f802,f575,f571,f806,f798,f563]) ).
fof(f999,plain,
( m1_subset_1(sK2,u1_struct_0(sK0))
| ~ r3_lattices(sK0,sK1,sK2)
| v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl30_19 ),
inference(resolution,[],[f808,f559]) ).
fof(f1001,plain,
( ~ r3_lattices(sK0,sK1,sK2)
| v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f999,f405]) ).
fof(f1002,plain,
( v12_lattices(sK0)
| ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f1001,f185]) ).
fof(f1003,plain,
( ~ l3_lattices(sK0)
| v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_16
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f1002,f793]) ).
fof(f1004,plain,
( v16_lattices(sK0)
| ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_16
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f1003,f186]) ).
fof(f1005,plain,
( ~ v15_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_15
| spl30_16
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f1004,f789]) ).
fof(f1006,plain,
( v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_15
| spl30_16
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f1005,f617]) ).
fof(f1007,plain,
( v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_15
| spl30_16
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f1006,f401]) ).
fof(f1008,plain,
( m1_subset_1(sK1,u1_struct_0(sK0))
| spl30_15
| spl30_16
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f1007,f189]) ).
fof(f1009,plain,
( $false
| spl30_15
| spl30_16
| ~ spl30_19 ),
inference(forward_subsumption_resolution,[],[f1008,f402]) ).
fof(f1010,plain,
( spl30_15
| spl30_16
| ~ spl30_19 ),
inference(avatar_contradiction_clause,[],[f1009]) ).
fof(f1011,plain,
( ~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| v11_lattices(sK0)
| ~ spl30_17
| ~ spl30_30 ),
inference(forward_subsumption_resolution,[],[f891,f902]) ).
fof(f1012,plain,
( v11_lattices(sK0)
| ~ spl30_17
| ~ spl30_29
| ~ spl30_30 ),
inference(forward_subsumption_resolution,[],[f1011,f898]) ).
fof(f1013,plain,
( spl30_28
| ~ spl30_17
| ~ spl30_29
| ~ spl30_30 ),
inference(avatar_split_clause,[],[f1012,f901,f897,f798,f893]) ).
fof(f1021,plain,
( v17_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_28 ),
inference(resolution,[],[f895,f417]) ).
fof(f1022,plain,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_28 ),
inference(forward_subsumption_resolution,[],[f1021,f404]) ).
fof(f1023,plain,
( ~ l3_lattices(sK0)
| ~ spl30_28 ),
inference(forward_subsumption_resolution,[],[f1022,f189]) ).
fof(f1024,plain,
( $false
| ~ spl30_28 ),
inference(forward_subsumption_resolution,[],[f1023,f186]) ).
fof(f1025,plain,
~ spl30_28,
inference(avatar_contradiction_clause,[],[f1024]) ).
fof(f1027,plain,
( ~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| ~ l3_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_1 ),
inference(resolution,[],[f565,f472]) ).
fof(f1029,plain,
( ~ l3_lattices(sK0)
| v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_1
| ~ spl30_29 ),
inference(forward_subsumption_resolution,[],[f1027,f898]) ).
fof(f1031,plain,
( v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_1
| ~ spl30_29 ),
inference(forward_subsumption_resolution,[],[f1029,f186]) ).
fof(f1033,plain,
( v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_1
| ~ spl30_29 ),
inference(forward_subsumption_resolution,[],[f1031,f401]) ).
fof(f1035,plain,
( ~ m2_lattice4(k22_filter_2(sK0,sK1,sK2),sK0)
| ~ spl30_1
| ~ spl30_29 ),
inference(forward_subsumption_resolution,[],[f1033,f189]) ).
fof(f1037,plain,
( $false
| ~ spl30_1
| ~ spl30_29
| ~ spl30_30 ),
inference(forward_subsumption_resolution,[],[f1035,f902]) ).
fof(f1038,plain,
( ~ spl30_1
| ~ spl30_29
| ~ spl30_30 ),
inference(avatar_contradiction_clause,[],[f1037]) ).
cnf(s1,plain,
( spl30_1
| spl30_2
| spl30_3
| ~ spl30_4 ),
inference(sat_conversion,[],[f578]) ).
cnf(s12,plain,
( spl30_4
| spl30_15
| spl30_16 ),
inference(sat_conversion,[],[f795]) ).
cnf(s14,plain,
( spl30_15
| spl30_16
| spl30_18 ),
inference(sat_conversion,[],[f818]) ).
cnf(s15,plain,
~ spl30_15,
inference(sat_conversion,[],[f823]) ).
cnf(s16,plain,
~ spl30_16,
inference(sat_conversion,[],[f843]) ).
cnf(s19,plain,
spl30_29,
inference(sat_conversion,[],[f928]) ).
cnf(s21,plain,
spl30_30,
inference(sat_conversion,[],[f946]) ).
cnf(s23,plain,
( ~ spl30_2
| ~ spl30_29
| ~ spl30_30 ),
inference(sat_conversion,[],[f985]) ).
cnf(s26,plain,
( spl30_1
| ~ spl30_3
| ~ spl30_4
| spl30_17
| ~ spl30_18
| spl30_19 ),
inference(sat_conversion,[],[f998]) ).
cnf(s27,plain,
( spl30_15
| spl30_16
| ~ spl30_19 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s28,plain,
( ~ spl30_17
| spl30_28
| ~ spl30_29
| ~ spl30_30 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s30,plain,
~ spl30_28,
inference(sat_conversion,[],[f1025]) ).
cnf(s31,plain,
( ~ spl30_1
| ~ spl30_29
| ~ spl30_30 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s33,plain,
( ~ spl30_17
| ~ spl30_29
| ~ spl30_30 ),
inference(rat,[],[s28,s30]) ).
cnf(s34,plain,
~ spl30_1,
inference(rat,[],[s31,s21,s19]) ).
cnf(s35,plain,
~ spl30_17,
inference(rat,[],[s33,s21,s19]) ).
cnf(s36,plain,
~ spl30_2,
inference(rat,[],[s23,s21,s19]) ).
cnf(s37,plain,
~ spl30_19,
inference(rat,[],[s27,s16,s15]) ).
cnf(s38,plain,
spl30_18,
inference(rat,[],[s14,s16,s15]) ).
cnf(s40,plain,
spl30_4,
inference(rat,[],[s12,s16,s15]) ).
cnf(s41,plain,
~ spl30_3,
inference(rat,[],[s26,s37,s38,s35,s34,s40]) ).
cnf(s47,plain,
$false,
inference(rat,[],[s1,s40,s41,s36,s34]) ).
fof(f1045,plain,
$false,
inference(avatar_sat_refutation,[],[s47]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT337+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.41 % Computer : n017.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 14:42:05 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.47 Running first-order model finding
% 0.15/0.47 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.23/0.56 % (2644825)Will run a generic schedule for satisfiability detection.
% 0.23/0.56 % (2644833)dis+10_1_sil=32000:sp=arity:random_seed=1757745418:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.23/0.56 % (2644830)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1667632340_2999 on theBenchmark for (2999ds/0Mi)
% 0.23/0.56 % (2644831)% WARNING: option uhcvi not known.
% 0.23/0.56 % (2644831)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2610801745:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.23/0.56 % (2644835)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2374758263:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.23/0.56 % (2644834)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=681269261:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.23/0.56 % (2644832)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1818013207:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.23/0.56 % TRYING [1]
% 0.23/0.56 % TRYING [2]
% 0.23/0.56 % (2644836)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2181954704:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.23/0.56 % TRYING [3]
% 0.23/0.56 % TRYING [4]
% 0.23/0.56 % (2644831) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2644825-2644831"...
% 0.23/0.56 % (2644831)...printing done.
% 0.23/0.56 % (2644831)Refutation found. Thanks to Tanya!
% 0.23/0.56 % SZS status Theorem for theBenchmark
% 0.23/0.56 % SZS output start Proof for theBenchmark
% See solution above
% 0.23/0.56 % (2644831)------------------------------
% 0.23/0.56 % (2644831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.56 % (2644831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.56 % (2644831)CaDiCaL version: 2.1.3
% 0.23/0.56 % (2644831)Termination reason: Refutation
% 0.23/0.56 % (2644831)Time elapsed: 0.033 s
% 0.23/0.56 % (2644831)Peak memory usage: 13 MB
% 0.23/0.56 % (2644831)Instructions burned: 32 (million)
% 0.23/0.56 % (2644825)Success in time 0.074 s
% 0.23/0.56 % Vampire exiting
%------------------------------------------------------------------------------