%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT310+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:47 AM UTC 2026
% Result : Theorem 8.39s 2.98s
% Output : Refutation 11.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 29
% Syntax : Number of formulae : 230 ( 35 unt; 15 def)
% Number of atoms : 975 ( 48 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 1241 ( 496 ~; 550 |; 143 &)
% ( 19 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 16 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-3 aty)
% Number of variables : 168 ( 0 sgn 157 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f70,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X0,X1)
& r1_tarski(X1,X2) )
=> r1_tarski(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f9363,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9463,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f12317,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f13529,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_2) ).
fof(f13532,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f13541,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m1_filter_2(k3_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_filter_2) ).
fof(f13547,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_filter_2) ).
fof(f13567,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m2_filter_2(k19_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k19_filter_2) ).
fof(f13601,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f13623,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( m2_filter_2(X3,X0)
=> ( r1_tarski(X1,X3)
=> r1_tarski(X2,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d11_filter_2) ).
fof(f13625,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_filter_2) ).
fof(f13627,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X3] :
( ( ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( ( r1_tarski(X2,X3)
=> r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3)) )
& r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_filter_2) ).
fof(f13628,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X3] :
( ( ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( ( r1_tarski(X2,X3)
=> r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3)) )
& r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13627]) ).
fof(f13655,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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)) ) ),
inference(pure_predicate_removal,[],[f9363]) ).
fof(f13712,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13529]) ).
fof(f13713,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13712]) ).
fof(f13718,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13532]) ).
fof(f13719,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13718]) ).
fof(f13736,plain,
! [X0,X1] :
( m1_filter_2(k3_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f13541]) ).
fof(f13737,plain,
! [X0,X1] :
( m1_filter_2(k3_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f13736]) ).
fof(f13748,plain,
! [X0,X1] :
( m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f13547]) ).
fof(f13749,plain,
! [X0,X1] :
( m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f13748]) ).
fof(f13788,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f13567]) ).
fof(f13789,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f13788]) ).
fof(f13843,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13601]) ).
fof(f13844,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13843]) ).
fof(f13887,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13623]) ).
fof(f13888,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13887]) ).
fof(f13891,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13625]) ).
fof(f13892,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13891]) ).
fof(f13895,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ( ~ r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3))
& r1_tarski(X2,X3) )
| ~ r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) )
& ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13628]) ).
fof(f13896,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ( ~ r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3))
& r1_tarski(X2,X3) )
| ~ r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) )
& ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f13895]) ).
fof(f13907,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12317]) ).
fof(f13908,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13907]) ).
fof(f14024,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f14027,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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,[],[f13655]) ).
fof(f14028,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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,[],[f14027]) ).
fof(f14255,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f14256,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(flattening,[],[f14255]) ).
fof(f14321,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13888]) ).
fof(f14322,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14321]) ).
fof(f14323,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f14322]) ).
fof(f14324,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK25(X0,X1,X2))
& r1_tarski(X1,sK25(X0,X1,X2))
& m2_filter_2(sK25(X0,X1,X2),X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(X3,sK25(X0,X1,X2))],[f14323]) ).
fof(f14325,plain,
( ( ( ~ r1_tarski(k19_filter_2(sK26,sK28),k19_filter_2(sK26,sK29))
& r1_tarski(sK28,sK29) )
| ~ r1_tarski(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),k19_filter_2(sK26,sK27)) )
& ~ v1_xboole_0(sK29)
& m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
& ~ v1_xboole_0(sK28)
& m1_subset_1(sK28,k1_zfmisc_1(u1_struct_0(sK26)))
& ~ v1_xboole_0(sK27)
& m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
& ~ v3_struct_0(sK26)
& v10_lattices(sK26)
& l3_lattices(sK26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26,sK27,sK28,sK29]),skolemize(X0,sK26),skolemize(X1,sK27),skolemize(X2,sK28),skolemize(X3,sK29)],[f13896]) ).
fof(f14443,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f14444,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f14443]) ).
fof(f14461,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13713]) ).
fof(f14465,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13719]) ).
fof(f14466,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13719]) ).
fof(f14476,plain,
! [X0,X1] :
( m1_filter_2(k3_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f13737]) ).
fof(f14482,plain,
! [X0,X1] :
( m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f13749]) ).
fof(f14504,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f13789]) ).
fof(f14568,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13844]) ).
fof(f14618,plain,
! [X2,X0,X1,X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0)
| k19_filter_2(X0,X1) != X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14324]) ).
fof(f14619,plain,
! [X2,X0,X1] :
( r1_tarski(X1,X2)
| k19_filter_2(X0,X1) != X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14324]) ).
fof(f14628,plain,
! [X2,X0,X1] :
( k19_filter_2(X0,X1) = k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13892]) ).
fof(f14630,plain,
l3_lattices(sK26),
inference(cnf_transformation,[],[f14325]) ).
fof(f14631,plain,
v10_lattices(sK26),
inference(cnf_transformation,[],[f14325]) ).
fof(f14632,plain,
~ v3_struct_0(sK26),
inference(cnf_transformation,[],[f14325]) ).
fof(f14633,plain,
m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26))),
inference(cnf_transformation,[],[f14325]) ).
fof(f14634,plain,
~ v1_xboole_0(sK27),
inference(cnf_transformation,[],[f14325]) ).
fof(f14635,plain,
m1_subset_1(sK28,k1_zfmisc_1(u1_struct_0(sK26))),
inference(cnf_transformation,[],[f14325]) ).
fof(f14636,plain,
~ v1_xboole_0(sK28),
inference(cnf_transformation,[],[f14325]) ).
fof(f14637,plain,
m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26))),
inference(cnf_transformation,[],[f14325]) ).
fof(f14638,plain,
~ v1_xboole_0(sK29),
inference(cnf_transformation,[],[f14325]) ).
fof(f14639,plain,
( r1_tarski(sK28,sK29)
| ~ r1_tarski(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),k19_filter_2(sK26,sK27)) ),
inference(cnf_transformation,[],[f14325]) ).
fof(f14640,plain,
( ~ r1_tarski(k19_filter_2(sK26,sK28),k19_filter_2(sK26,sK29))
| ~ r1_tarski(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),k19_filter_2(sK26,sK27)) ),
inference(cnf_transformation,[],[f14325]) ).
fof(f14659,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13908]) ).
fof(f14779,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14024]) ).
fof(f14782,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14028]) ).
fof(f14789,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14028]) ).
fof(f15130,plain,
! [X2,X0,X1] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(cnf_transformation,[],[f14256]) ).
fof(f15132,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f14444]) ).
fof(f15177,plain,
! [X0,X1] :
( r1_tarski(X1,k19_filter_2(X0,X1))
| ~ m2_filter_2(k19_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f14619]) ).
fof(f15178,plain,
! [X0,X1,X4] :
( r1_tarski(k19_filter_2(X0,X1),X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0)
| ~ m2_filter_2(k19_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f14618]) ).
fof(f15205,plain,
! [X1] : r1_tarski(X1,X1),
inference(equality_resolution,[],[f15132]) ).
fof(f15237,definition,
( spl102_1
<=> r1_tarski(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),k19_filter_2(sK26,sK27)) ),
introduced(definition,[new_symbols(definition,[spl102_1])],[avatar_definition]) ).
fof(f15238,plain,
( ~ r1_tarski(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),k19_filter_2(sK26,sK27))
| spl102_1 ),
inference(avatar_component_clause,[],[f15237]) ).
fof(f15240,definition,
( spl102_2
<=> r1_tarski(sK28,sK29) ),
introduced(definition,[new_symbols(definition,[spl102_2])],[avatar_definition]) ).
fof(f15241,plain,
( r1_tarski(sK28,sK29)
| ~ spl102_2 ),
inference(avatar_component_clause,[],[f15240]) ).
fof(f15242,plain,
( ~ spl102_1
| spl102_2 ),
inference(avatar_split_clause,[],[f14639,f15240,f15237]) ).
fof(f15244,definition,
( spl102_3
<=> r1_tarski(k19_filter_2(sK26,sK28),k19_filter_2(sK26,sK29)) ),
introduced(definition,[new_symbols(definition,[spl102_3])],[avatar_definition]) ).
fof(f15245,plain,
( ~ r1_tarski(k19_filter_2(sK26,sK28),k19_filter_2(sK26,sK29))
| spl102_3 ),
inference(avatar_component_clause,[],[f15244]) ).
fof(f15246,plain,
( ~ spl102_1
| ~ spl102_3 ),
inference(avatar_split_clause,[],[f14640,f15244,f15237]) ).
fof(f15251,plain,
( sK27 = k7_filter_2(sK26,sK27)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f14633,f14568]) ).
fof(f15265,plain,
( sK27 = k7_filter_2(sK26,sK27)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f15251,f14632]) ).
fof(f15271,plain,
( sK27 = k7_filter_2(sK26,sK27)
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f15265,f14631]) ).
fof(f15277,plain,
sK27 = k7_filter_2(sK26,sK27),
inference(forward_subsumption_resolution,[],[f15271,f14630]) ).
fof(f15405,definition,
( spl102_19
<=> m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26))) ),
introduced(definition,[new_symbols(definition,[spl102_19])],[avatar_definition]) ).
fof(f15406,plain,
( ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_19 ),
inference(avatar_component_clause,[],[f15405]) ).
fof(f15408,definition,
( spl102_20
<=> m2_filter_2(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),sK26) ),
introduced(definition,[new_symbols(definition,[spl102_20])],[avatar_definition]) ).
fof(f15409,plain,
( ~ m2_filter_2(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),sK26)
| spl102_20 ),
inference(avatar_component_clause,[],[f15408]) ).
fof(f15411,definition,
( spl102_21
<=> m2_filter_2(k19_filter_2(sK26,sK27),sK26) ),
introduced(definition,[new_symbols(definition,[spl102_21])],[avatar_definition]) ).
fof(f15412,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| spl102_21 ),
inference(avatar_component_clause,[],[f15411]) ).
fof(f15488,plain,
! [X0] :
( k19_filter_2(sK26,sK27) = k3_filter_2(k1_lattice2(sK26),sK27)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| v1_xboole_0(sK27)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26) ),
inference(superposition,[],[f14628,f15277]) ).
fof(f15489,plain,
( m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(superposition,[],[f14482,f15277]) ).
fof(f15490,plain,
( m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f15489,f14632]) ).
fof(f15491,plain,
! [X0] :
( k19_filter_2(sK26,sK27) = k3_filter_2(k1_lattice2(sK26),sK27)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f15488,f14634]) ).
fof(f15493,plain,
( m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| ~ l3_lattices(sK26)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f15490,f14631]) ).
fof(f15494,plain,
! [X0] :
( k19_filter_2(sK26,sK27) = k3_filter_2(k1_lattice2(sK26),sK27)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f15491,f14633]) ).
fof(f15496,plain,
( m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f15493,f14630]) ).
fof(f15497,plain,
! [X0] :
( k19_filter_2(sK26,sK27) = k3_filter_2(k1_lattice2(sK26),sK27)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f15494,f14632]) ).
fof(f15499,plain,
m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26)))),
inference(forward_subsumption_resolution,[],[f15496,f14633]) ).
fof(f15500,plain,
! [X0] :
( k19_filter_2(sK26,sK27) = k3_filter_2(k1_lattice2(sK26),sK27)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f15497,f14631]) ).
fof(f15502,plain,
! [X0] :
( k19_filter_2(sK26,sK27) = k3_filter_2(k1_lattice2(sK26),sK27)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26)))) ),
inference(forward_subsumption_resolution,[],[f15500,f14630]) ).
fof(f15505,definition,
( spl102_31
<=> ! [X0] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26)))) ) ),
introduced(definition,[new_symbols(definition,[spl102_31])],[avatar_definition]) ).
fof(f15506,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| v1_xboole_0(X0) )
| ~ spl102_31 ),
inference(avatar_component_clause,[],[f15505]) ).
fof(f15508,definition,
( spl102_32
<=> k19_filter_2(sK26,sK27) = k3_filter_2(k1_lattice2(sK26),sK27) ),
introduced(definition,[new_symbols(definition,[spl102_32])],[avatar_definition]) ).
fof(f15509,plain,
( k19_filter_2(sK26,sK27) = k3_filter_2(k1_lattice2(sK26),sK27)
| ~ spl102_32 ),
inference(avatar_component_clause,[],[f15508]) ).
fof(f15510,plain,
( spl102_31
| spl102_32 ),
inference(avatar_split_clause,[],[f15502,f15508,f15505]) ).
fof(f15625,plain,
( ~ m2_lattice4(k19_filter_2(sK26,sK27),sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_19 ),
inference(resolution,[],[f15406,f14659]) ).
fof(f15633,plain,
( ~ m2_lattice4(k19_filter_2(sK26,sK27),sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_19 ),
inference(forward_subsumption_resolution,[],[f15625,f14632]) ).
fof(f15636,plain,
( ~ m2_lattice4(k19_filter_2(sK26,sK27),sK26)
| ~ l3_lattices(sK26)
| spl102_19 ),
inference(forward_subsumption_resolution,[],[f15633,f14631]) ).
fof(f15639,plain,
( ~ m2_lattice4(k19_filter_2(sK26,sK27),sK26)
| spl102_19 ),
inference(forward_subsumption_resolution,[],[f15636,f14630]) ).
fof(f15876,plain,
( ~ r1_tarski(sK28,k19_filter_2(sK26,sK29))
| ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| ~ m2_filter_2(k19_filter_2(sK26,sK28),sK26)
| v1_xboole_0(sK28)
| ~ m1_subset_1(sK28,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_3 ),
inference(resolution,[],[f15245,f15178]) ).
fof(f15878,plain,
( ~ r1_tarski(sK28,k19_filter_2(sK26,sK29))
| ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| v1_xboole_0(sK28)
| ~ m1_subset_1(sK28,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_3 ),
inference(forward_subsumption_resolution,[],[f15876,f14504]) ).
fof(f15879,plain,
( ~ r1_tarski(sK28,k19_filter_2(sK26,sK29))
| ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| ~ m1_subset_1(sK28,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_3 ),
inference(forward_subsumption_resolution,[],[f15878,f14636]) ).
fof(f15880,plain,
( ~ r1_tarski(sK28,k19_filter_2(sK26,sK29))
| ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_3 ),
inference(forward_subsumption_resolution,[],[f15879,f14635]) ).
fof(f15881,plain,
( ~ r1_tarski(sK28,k19_filter_2(sK26,sK29))
| ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_3 ),
inference(forward_subsumption_resolution,[],[f15880,f14632]) ).
fof(f15882,plain,
( ~ r1_tarski(sK28,k19_filter_2(sK26,sK29))
| ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| ~ l3_lattices(sK26)
| spl102_3 ),
inference(forward_subsumption_resolution,[],[f15881,f14631]) ).
fof(f15883,plain,
( ~ r1_tarski(sK28,k19_filter_2(sK26,sK29))
| ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| spl102_3 ),
inference(forward_subsumption_resolution,[],[f15882,f14630]) ).
fof(f15885,definition,
( spl102_50
<=> m2_filter_2(k19_filter_2(sK26,sK29),sK26) ),
introduced(definition,[new_symbols(definition,[spl102_50])],[avatar_definition]) ).
fof(f15886,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| spl102_50 ),
inference(avatar_component_clause,[],[f15885]) ).
fof(f15888,definition,
( spl102_51
<=> r1_tarski(sK28,k19_filter_2(sK26,sK29)) ),
introduced(definition,[new_symbols(definition,[spl102_51])],[avatar_definition]) ).
fof(f15889,plain,
( ~ r1_tarski(sK28,k19_filter_2(sK26,sK29))
| spl102_51 ),
inference(avatar_component_clause,[],[f15888]) ).
fof(f15890,plain,
( ~ spl102_50
| ~ spl102_51
| spl102_3 ),
inference(avatar_split_clause,[],[f15883,f15244,f15888,f15885]) ).
fof(f15897,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_50 ),
inference(resolution,[],[f15886,f14504]) ).
fof(f15898,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_50 ),
inference(forward_subsumption_resolution,[],[f15897,f14632]) ).
fof(f15899,plain,
( ~ l3_lattices(sK26)
| v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_50 ),
inference(forward_subsumption_resolution,[],[f15898,f14631]) ).
fof(f15900,plain,
( v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_50 ),
inference(forward_subsumption_resolution,[],[f15899,f14630]) ).
fof(f15901,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_50 ),
inference(forward_subsumption_resolution,[],[f15900,f14638]) ).
fof(f15902,plain,
( $false
| spl102_50 ),
inference(forward_subsumption_resolution,[],[f15901,f14637]) ).
fof(f15903,plain,
spl102_50,
inference(avatar_contradiction_clause,[],[f15902]) ).
fof(f15908,plain,
( ! [X0] :
( ~ r1_tarski(X0,k19_filter_2(sK26,sK29))
| ~ r1_tarski(sK28,X0) )
| spl102_51 ),
inference(resolution,[],[f15889,f15130]) ).
fof(f15985,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_19 ),
inference(resolution,[],[f15639,f14465]) ).
fof(f15988,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_19 ),
inference(forward_subsumption_resolution,[],[f15985,f14632]) ).
fof(f15991,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| ~ l3_lattices(sK26)
| spl102_19 ),
inference(forward_subsumption_resolution,[],[f15988,f14631]) ).
fof(f15994,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| spl102_19 ),
inference(forward_subsumption_resolution,[],[f15991,f14630]) ).
fof(f15996,plain,
( ~ spl102_21
| spl102_19 ),
inference(avatar_split_clause,[],[f15994,f15405,f15411]) ).
fof(f15997,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| v1_xboole_0(sK27)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_21 ),
inference(resolution,[],[f15412,f14504]) ).
fof(f15998,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| v1_xboole_0(sK27)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_21 ),
inference(forward_subsumption_resolution,[],[f15997,f14632]) ).
fof(f15999,plain,
( ~ l3_lattices(sK26)
| v1_xboole_0(sK27)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_21 ),
inference(forward_subsumption_resolution,[],[f15998,f14631]) ).
fof(f16000,plain,
( v1_xboole_0(sK27)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_21 ),
inference(forward_subsumption_resolution,[],[f15999,f14630]) ).
fof(f16001,plain,
( ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_21 ),
inference(forward_subsumption_resolution,[],[f16000,f14634]) ).
fof(f16002,plain,
( $false
| spl102_21 ),
inference(forward_subsumption_resolution,[],[f16001,f14633]) ).
fof(f16003,plain,
spl102_21,
inference(avatar_contradiction_clause,[],[f16002]) ).
fof(f16012,definition,
( spl102_57
<=> v1_xboole_0(k19_filter_2(sK26,sK27)) ),
introduced(definition,[new_symbols(definition,[spl102_57])],[avatar_definition]) ).
fof(f16013,plain,
( v1_xboole_0(k19_filter_2(sK26,sK27))
| ~ spl102_57 ),
inference(avatar_component_clause,[],[f16012]) ).
fof(f16023,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| v1_xboole_0(k19_filter_2(sK26,sK27))
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_20 ),
inference(resolution,[],[f15409,f14504]) ).
fof(f16024,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| v1_xboole_0(k19_filter_2(sK26,sK27))
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_20 ),
inference(forward_subsumption_resolution,[],[f16023,f14632]) ).
fof(f16025,plain,
( ~ l3_lattices(sK26)
| v1_xboole_0(k19_filter_2(sK26,sK27))
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_20 ),
inference(forward_subsumption_resolution,[],[f16024,f14631]) ).
fof(f16026,plain,
( v1_xboole_0(k19_filter_2(sK26,sK27))
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_20 ),
inference(forward_subsumption_resolution,[],[f16025,f14630]) ).
fof(f16027,plain,
( ~ spl102_19
| spl102_57
| spl102_20 ),
inference(avatar_split_clause,[],[f16026,f15408,f16012,f15405]) ).
fof(f16383,definition,
( spl102_70
<=> l3_lattices(k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl102_70])],[avatar_definition]) ).
fof(f16384,plain,
( ~ l3_lattices(k1_lattice2(sK26))
| spl102_70 ),
inference(avatar_component_clause,[],[f16383]) ).
fof(f16386,definition,
( spl102_71
<=> v10_lattices(k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl102_71])],[avatar_definition]) ).
fof(f16387,plain,
( ~ v10_lattices(k1_lattice2(sK26))
| spl102_71 ),
inference(avatar_component_clause,[],[f16386]) ).
fof(f16389,definition,
( spl102_72
<=> v3_struct_0(k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl102_72])],[avatar_definition]) ).
fof(f16390,plain,
( v3_struct_0(k1_lattice2(sK26))
| ~ spl102_72 ),
inference(avatar_component_clause,[],[f16389]) ).
fof(f16436,plain,
( ~ l3_lattices(sK26)
| spl102_70 ),
inference(resolution,[],[f16384,f14779]) ).
fof(f16439,plain,
( $false
| spl102_70 ),
inference(forward_subsumption_resolution,[],[f16436,f14630]) ).
fof(f16440,plain,
spl102_70,
inference(avatar_contradiction_clause,[],[f16439]) ).
fof(f16498,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_71 ),
inference(resolution,[],[f16387,f14782]) ).
fof(f16502,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_71 ),
inference(forward_subsumption_resolution,[],[f16498,f14632]) ).
fof(f16504,plain,
( ~ l3_lattices(sK26)
| spl102_71 ),
inference(forward_subsumption_resolution,[],[f16502,f14631]) ).
fof(f16506,plain,
( $false
| spl102_71 ),
inference(forward_subsumption_resolution,[],[f16504,f14630]) ).
fof(f16507,plain,
spl102_71,
inference(avatar_contradiction_clause,[],[f16506]) ).
fof(f16564,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl102_72 ),
inference(resolution,[],[f16390,f14789]) ).
fof(f16567,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl102_72 ),
inference(forward_subsumption_resolution,[],[f16564,f14632]) ).
fof(f16570,plain,
( ~ l3_lattices(sK26)
| ~ spl102_72 ),
inference(forward_subsumption_resolution,[],[f16567,f14631]) ).
fof(f16574,plain,
( $false
| ~ spl102_72 ),
inference(forward_subsumption_resolution,[],[f16570,f14630]) ).
fof(f16575,plain,
~ spl102_72,
inference(avatar_contradiction_clause,[],[f16574]) ).
fof(f16642,plain,
( v1_xboole_0(sK27)
| ~ spl102_31 ),
inference(resolution,[],[f15506,f15499]) ).
fof(f16680,plain,
( $false
| ~ spl102_31 ),
inference(forward_subsumption_resolution,[],[f16642,f14634]) ).
fof(f16681,plain,
~ spl102_31,
inference(avatar_contradiction_clause,[],[f16680]) ).
fof(f16712,plain,
( m1_filter_2(k19_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| v1_xboole_0(sK27)
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| ~ spl102_32 ),
inference(superposition,[],[f14476,f15509]) ).
fof(f16713,plain,
( m1_filter_2(k19_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK26))))
| ~ spl102_32 ),
inference(forward_subsumption_resolution,[],[f16712,f14634]) ).
fof(f16716,plain,
( m1_filter_2(k19_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ spl102_32 ),
inference(forward_subsumption_resolution,[],[f16713,f15499]) ).
fof(f16720,definition,
( spl102_106
<=> m1_filter_2(k19_filter_2(sK26,sK27),k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl102_106])],[avatar_definition]) ).
fof(f16721,plain,
( m1_filter_2(k19_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ spl102_106 ),
inference(avatar_component_clause,[],[f16720]) ).
fof(f16722,plain,
( ~ spl102_70
| ~ spl102_71
| spl102_72
| spl102_106
| ~ spl102_32 ),
inference(avatar_split_clause,[],[f16716,f15508,f16720,f16389,f16386,f16383]) ).
fof(f16908,plain,
( ~ r1_tarski(sK28,sK29)
| ~ m2_filter_2(k19_filter_2(sK26,sK29),sK26)
| v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_51 ),
inference(resolution,[],[f15908,f15177]) ).
fof(f16918,plain,
( ~ r1_tarski(sK28,sK29)
| v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_51 ),
inference(forward_subsumption_resolution,[],[f16908,f14504]) ).
fof(f16919,plain,
( v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl102_2
| spl102_51 ),
inference(forward_subsumption_resolution,[],[f16918,f15241]) ).
fof(f16920,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl102_2
| spl102_51 ),
inference(forward_subsumption_resolution,[],[f16919,f14638]) ).
fof(f16921,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl102_2
| spl102_51 ),
inference(forward_subsumption_resolution,[],[f16920,f14637]) ).
fof(f16922,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl102_2
| spl102_51 ),
inference(forward_subsumption_resolution,[],[f16921,f14632]) ).
fof(f16923,plain,
( ~ l3_lattices(sK26)
| ~ spl102_2
| spl102_51 ),
inference(forward_subsumption_resolution,[],[f16922,f14631]) ).
fof(f16924,plain,
( $false
| ~ spl102_2
| spl102_51 ),
inference(forward_subsumption_resolution,[],[f16923,f14630]) ).
fof(f16925,plain,
( ~ spl102_2
| spl102_51 ),
inference(avatar_contradiction_clause,[],[f16924]) ).
fof(f16926,plain,
( ~ r1_tarski(k19_filter_2(sK26,sK27),k19_filter_2(sK26,sK27))
| ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| ~ m2_filter_2(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),sK26)
| v1_xboole_0(k19_filter_2(sK26,sK27))
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_1 ),
inference(resolution,[],[f15238,f15178]) ).
fof(f16928,plain,
( ~ r1_tarski(k19_filter_2(sK26,sK27),k19_filter_2(sK26,sK27))
| ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| ~ m2_filter_2(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),sK26)
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_1 ),
inference(forward_subsumption_resolution,[],[f16926,f14466]) ).
fof(f16929,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| ~ m2_filter_2(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),sK26)
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_1 ),
inference(forward_subsumption_resolution,[],[f16928,f15205]) ).
fof(f16930,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| ~ m2_filter_2(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),sK26)
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl102_1 ),
inference(forward_subsumption_resolution,[],[f16929,f14632]) ).
fof(f16931,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| ~ m2_filter_2(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),sK26)
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| ~ l3_lattices(sK26)
| spl102_1 ),
inference(forward_subsumption_resolution,[],[f16930,f14631]) ).
fof(f16932,plain,
( ~ m2_filter_2(k19_filter_2(sK26,sK27),sK26)
| ~ m2_filter_2(k19_filter_2(sK26,k19_filter_2(sK26,sK27)),sK26)
| ~ m1_subset_1(k19_filter_2(sK26,sK27),k1_zfmisc_1(u1_struct_0(sK26)))
| spl102_1 ),
inference(forward_subsumption_resolution,[],[f16931,f14630]) ).
fof(f16933,plain,
( ~ spl102_19
| ~ spl102_20
| ~ spl102_21
| spl102_1 ),
inference(avatar_split_clause,[],[f16932,f15237,f15411,f15408,f15405]) ).
fof(f18804,plain,
( ~ v1_xboole_0(k19_filter_2(sK26,sK27))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ spl102_106 ),
inference(resolution,[],[f16721,f14461]) ).
fof(f18805,plain,
( v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ spl102_57
| ~ spl102_106 ),
inference(forward_subsumption_resolution,[],[f18804,f16013]) ).
fof(f18807,plain,
( ~ spl102_70
| ~ spl102_71
| spl102_72
| ~ spl102_57
| ~ spl102_106 ),
inference(avatar_split_clause,[],[f18805,f16720,f16012,f16389,f16386,f16383]) ).
cnf(s1,plain,
( ~ spl102_1
| spl102_2 ),
inference(sat_conversion,[],[f15242]) ).
cnf(s2,plain,
( ~ spl102_1
| ~ spl102_3 ),
inference(sat_conversion,[],[f15246]) ).
cnf(s17,plain,
( spl102_31
| spl102_32 ),
inference(sat_conversion,[],[f15510]) ).
cnf(s32,plain,
( spl102_3
| ~ spl102_50
| ~ spl102_51 ),
inference(sat_conversion,[],[f15890]) ).
cnf(s33,plain,
spl102_50,
inference(sat_conversion,[],[f15903]) ).
cnf(s42,plain,
( spl102_19
| ~ spl102_21 ),
inference(sat_conversion,[],[f15996]) ).
cnf(s43,plain,
spl102_21,
inference(sat_conversion,[],[f16003]) ).
cnf(s46,plain,
( ~ spl102_19
| spl102_20
| spl102_57 ),
inference(sat_conversion,[],[f16027]) ).
cnf(s76,plain,
spl102_70,
inference(sat_conversion,[],[f16440]) ).
cnf(s84,plain,
spl102_71,
inference(sat_conversion,[],[f16507]) ).
cnf(s93,plain,
~ spl102_72,
inference(sat_conversion,[],[f16575]) ).
cnf(s99,plain,
~ spl102_31,
inference(sat_conversion,[],[f16681]) ).
cnf(s107,plain,
( ~ spl102_32
| ~ spl102_70
| ~ spl102_71
| spl102_72
| spl102_106 ),
inference(sat_conversion,[],[f16722]) ).
cnf(s130,plain,
( ~ spl102_2
| spl102_51 ),
inference(sat_conversion,[],[f16925]) ).
cnf(s131,plain,
( spl102_1
| ~ spl102_19
| ~ spl102_20
| ~ spl102_21 ),
inference(sat_conversion,[],[f16933]) ).
cnf(s209,plain,
( ~ spl102_57
| ~ spl102_70
| ~ spl102_71
| spl102_72
| ~ spl102_106 ),
inference(sat_conversion,[],[f18807]) ).
cnf(s249,plain,
spl102_19,
inference(rat,[],[s42,s43]) ).
cnf(s250,plain,
( spl102_3
| ~ spl102_51 ),
inference(rat,[],[s32,s33]) ).
cnf(s269,plain,
spl102_32,
inference(rat,[],[s17,s99]) ).
cnf(s271,plain,
spl102_106,
inference(rat,[],[s107,s76,s93,s84,s269]) ).
cnf(s272,plain,
~ spl102_57,
inference(rat,[],[s209,s76,s93,s84,s271]) ).
cnf(s273,plain,
spl102_20,
inference(rat,[],[s46,s249,s272]) ).
cnf(s274,plain,
spl102_1,
inference(rat,[],[s131,s43,s249,s273]) ).
cnf(s276,plain,
~ spl102_3,
inference(rat,[],[s2,s274]) ).
cnf(s277,plain,
~ spl102_51,
inference(rat,[],[s250,s276]) ).
cnf(s278,plain,
~ spl102_2,
inference(rat,[],[s130,s277]) ).
cnf(s280,plain,
$false,
inference(rat,[],[s1,s278,s274]) ).
fof(f18810,plain,
$false,
inference(avatar_sat_refutation,[],[s280]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT310+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n003.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 14:30:29 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/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
% 8.39/2.98 % (595725)Detected formulas, will run a generic FOF schedule.
% 8.39/2.98 % (595730)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=3670143073:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 8.39/2.98 % (595735)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=407271117:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 8.39/2.98 % (595733)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4129874222:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 8.39/2.98 % (595731)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=3729428102:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 8.39/2.98 % (595732)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=1144804079:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 8.39/2.98 % (595734)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1224959092:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 8.39/2.98 % (595736)dis-21_1_sil=8000:lcm=predicate:random_seed=960050611:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 8.39/2.98 % (595735)Instruction limit reached!
% 8.39/2.98 % (595735)------------------------------
% 8.39/2.98 % (595735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595735)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595735)Termination reason: Instruction limit
% 8.39/2.98 % (595735)Termination phase: Property scanning
% 8.39/2.98 % (595735)Time elapsed: 0.059 s
% 8.39/2.98 % (595735)Peak memory usage: 103 MB
% 8.39/2.98 % (595735)Instructions burned: 141 (million)
% 8.39/2.98 % (595733)Instruction limit reached!
% 8.39/2.98 % (595733)------------------------------
% 8.39/2.98 % (595733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595733)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595733)Termination reason: Instruction limit
% 8.39/2.98 % (595733)Termination phase: Saturation
% 8.39/2.98 % (595733)Time elapsed: 0.085 s
% 8.39/2.98 % (595733)Peak memory usage: 107 MB
% 8.39/2.98 % (595733)Instructions burned: 110 (million)
% 8.39/2.98 % (595734)Instruction limit reached!
% 8.39/2.98 % (595734)------------------------------
% 8.39/2.98 % (595734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595734)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595734)Termination reason: Instruction limit
% 8.39/2.98 % (595734)Termination phase: Equality resolution with deletion
% 8.39/2.98 % (595734)Time elapsed: 0.093 s
% 8.39/2.98 % (595734)Peak memory usage: 105 MB
% 8.39/2.98 % (595734)Instructions burned: 120 (million)
% 8.39/2.98 % (595736)Instruction limit reached!
% 8.39/2.98 % (595736)------------------------------
% 8.39/2.98 % (595736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595736)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595736)Termination reason: Instruction limit
% 8.39/2.98 % (595736)Termination phase: Preprocessing 1
% 8.39/2.98 % (595736)Time elapsed: 0.098 s
% 8.39/2.98 % (595736)Peak memory usage: 104 MB
% 8.39/2.98 % (595736)Instructions burned: 129 (million)
% 8.39/2.98 % (595744)lrs+10_1_sil=8000:sp=occurrence:random_seed=3503784186:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 8.39/2.98 % (595746)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2018349925:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 8.39/2.98 % (595745)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3712693604:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 8.39/2.98 % (595747)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=2270947536:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 8.39/2.98 % (595745)Instruction limit reached!
% 8.39/2.98 % (595745)------------------------------
% 8.39/2.98 % (595745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595745)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595745)Termination reason: Instruction limit
% 8.39/2.98 % (595745)Termination phase: Property scanning
% 8.39/2.98 % (595745)Time elapsed: 0.068 s
% 8.39/2.98 % (595745)Peak memory usage: 103 MB
% 8.39/2.98 % (595745)Instructions burned: 159 (million)
% 8.39/2.98 % (595747)Instruction limit reached!
% 8.39/2.98 % (595747)------------------------------
% 8.39/2.98 % (595747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595747)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595747)Termination reason: Instruction limit
% 8.39/2.98 % (595747)Termination phase: SInE selection
% 8.39/2.98 % (595747)Time elapsed: 0.125 s
% 8.39/2.98 % (595747)Peak memory usage: 103 MB
% 8.39/2.98 % (595747)Instructions burned: 249 (million)
% 8.39/2.98 % (595744)Instruction limit reached!
% 8.39/2.98 % (595744)------------------------------
% 8.39/2.98 % (595744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595744)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595744)Termination reason: Instruction limit
% 8.39/2.98 % (595744)Termination phase: Saturation
% 8.39/2.98 % (595744)Time elapsed: 0.201 s
% 8.39/2.98 % (595744)Peak memory usage: 110 MB
% 8.39/2.98 % (595744)Instructions burned: 285 (million)
% 8.39/2.98 % (595752)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1150758800:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 8.39/2.98 % (595746)Instruction limit reached!
% 8.39/2.98 % (595746)------------------------------
% 8.39/2.98 % (595746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595746)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595746)Termination reason: Instruction limit
% 8.39/2.98 % (595746)Termination phase: Saturation
% 8.39/2.98 % (595746)Time elapsed: 0.230 s
% 8.39/2.98 % (595746)Peak memory usage: 108 MB
% 8.39/2.98 % (595746)Instructions burned: 325 (million)
% 8.39/2.98 % (595753)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3822599169:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 8.39/2.98 % (595754)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3422366585:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 8.39/2.98 % (595756)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1904435355:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 8.39/2.98 % (595754)Instruction limit reached!
% 8.39/2.98 % (595754)------------------------------
% 8.39/2.98 % (595754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595754)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595754)Termination reason: Instruction limit
% 8.39/2.98 % (595754)Termination phase: Preprocessing 3
% 8.39/2.98 % (595754)Time elapsed: 0.093 s
% 8.39/2.98 % (595754)Peak memory usage: 105 MB
% 8.39/2.98 % (595754)Instructions burned: 115 (million)
% 8.39/2.98 % (595752)Instruction limit reached!
% 8.39/2.98 % (595752)------------------------------
% 8.39/2.98 % (595752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595752)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595752)Termination reason: Instruction limit
% 8.39/2.98 % (595752)Termination phase: Saturation
% 8.39/2.98 % (595752)Time elapsed: 0.194 s
% 8.39/2.98 % (595752)Peak memory usage: 109 MB
% 8.39/2.98 % (595752)Instructions burned: 297 (million)
% 8.39/2.98 % (595756)Instruction limit reached!
% 8.39/2.98 % (595756)------------------------------
% 8.39/2.98 % (595756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595756)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595756)Termination reason: Instruction limit
% 8.39/2.98 % (595756)Termination phase: Preprocessing 2
% 8.39/2.98 % (595756)Time elapsed: 0.100 s
% 8.39/2.98 % (595756)Peak memory usage: 106 MB
% 8.39/2.98 % (595756)Instructions burned: 127 (million)
% 8.39/2.98 % (595760)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=651394836:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 8.39/2.98 % (595761)lrs+10_1_sil=8000:sp=occurrence:random_seed=3381967617:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 8.39/2.98 % (595760)Instruction limit reached!
% 8.39/2.98 % (595760)------------------------------
% 8.39/2.98 % (595760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.98 % (595760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.98 % (595760)CaDiCaL version: 2.1.3
% 8.39/2.98 % (595760)Termination reason: Instruction limit
% 8.39/2.98 % (595760)Termination phase: Property scanning
% 8.39/2.98 % (595760)Time elapsed: 0.051 s
% 8.39/2.98 % (595760)Peak memory usage: 103 MB
% 8.39/2.98 % (595760)Instructions burned: 116 (million)
% 8.39/2.98 % (595762)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3191695836:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 8.39/2.98 % (595765)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3772202484:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 8.39/2.98 % (595762)First to succeed.
% 8.39/2.98 % (595762)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-595725"
% 8.39/2.98 % (595762)Refutation found. Thanks to Tanya!
% 8.39/2.98 % SZS status Theorem for theBenchmark
% 8.39/2.98 % SZS output start Proof for theBenchmark
% See solution above
% 11.40/3.18 % (595762)------------------------------
% 11.40/3.18 % (595762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.40/3.18 % (595762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.40/3.18 % (595762)CaDiCaL version: 2.1.3
% 11.40/3.18 % (595762)Termination reason: Refutation
% 11.40/3.18 % (595762)Time elapsed: 0.201 s
% 11.40/3.18 % (595762)Peak memory usage: 110 MB
% 11.40/3.18 % (595762)Instructions burned: 306 (million)
% 11.40/3.18 % (595762)------------------------------
% 11.40/3.18 % (595762)------------------------------
% 11.40/3.18 % (595725)Success in time 2.127 s
% 11.40/3.18 % Vampire exiting
%------------------------------------------------------------------------------