%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT310+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 10.67s 2.45s
% Output : Refutation 11.08s
% 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f2569,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f2669,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f2857,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f2870,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/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_2) ).
fof(f2873,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f2882,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/sandbox2/benchmark/theBenchmark.p',dt_k3_filter_2) ).
fof(f2888,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/sandbox2/benchmark/theBenchmark.p',dt_k7_filter_2) ).
fof(f2908,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/sandbox2/benchmark/theBenchmark.p',dt_k19_filter_2) ).
fof(f2942,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f2964,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/sandbox2/benchmark/theBenchmark.p',d11_filter_2) ).
fof(f2966,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/sandbox2/benchmark/theBenchmark.p',t37_filter_2) ).
fof(f2968,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/sandbox2/benchmark/theBenchmark.p',t39_filter_2) ).
fof(f2969,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)],[f2968]) ).
fof(f2993,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,[],[f2569]) ).
fof(f3011,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,[],[f2870]) ).
fof(f3012,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,[],[f3011]) ).
fof(f3017,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,[],[f2873]) ).
fof(f3018,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,[],[f3017]) ).
fof(f3035,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,[],[f2882]) ).
fof(f3036,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,[],[f3035]) ).
fof(f3047,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,[],[f2888]) ).
fof(f3048,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,[],[f3047]) ).
fof(f3087,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,[],[f2908]) ).
fof(f3088,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,[],[f3087]) ).
fof(f3152,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,[],[f2942]) ).
fof(f3153,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,[],[f3152]) ).
fof(f3196,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,[],[f2964]) ).
fof(f3197,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,[],[f3196]) ).
fof(f3200,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,[],[f2966]) ).
fof(f3201,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,[],[f3200]) ).
fof(f3204,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,[],[f2969]) ).
fof(f3205,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,[],[f3204]) ).
fof(f3215,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,[],[f2857]) ).
fof(f3216,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,[],[f3215]) ).
fof(f3328,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f3331,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,[],[f2993]) ).
fof(f3332,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,[],[f3331]) ).
fof(f3611,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f3612,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(flattening,[],[f3611]) ).
fof(f3670,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,[],[f3197]) ).
fof(f3671,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,[],[f3670]) ).
fof(f3672,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,[],[f3671]) ).
fof(f3673,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK22(X0,X1,X2))
& r1_tarski(X1,sK22(X0,X1,X2))
& m2_filter_2(sK22(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,[sK22]),skolemize(X3,sK22(X0,X1,X2))],[f3672]) ).
fof(f3674,plain,
( ( ( ~ r1_tarski(k19_filter_2(sK23,sK25),k19_filter_2(sK23,sK26))
& r1_tarski(sK25,sK26) )
| ~ r1_tarski(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),k19_filter_2(sK23,sK24)) )
& ~ v1_xboole_0(sK26)
& m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
& ~ v1_xboole_0(sK25)
& m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK23)))
& ~ v1_xboole_0(sK24)
& m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23)))
& ~ v3_struct_0(sK23)
& v10_lattices(sK23)
& l3_lattices(sK23) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24,sK25,sK26]),skolemize(X0,sK23),skolemize(X1,sK24),skolemize(X2,sK25),skolemize(X3,sK26)],[f3205]) ).
fof(f3849,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(f3850,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,[],[f3849]) ).
fof(f3867,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,[],[f3012]) ).
fof(f3871,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,[],[f3018]) ).
fof(f3872,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,[],[f3018]) ).
fof(f3882,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,[],[f3036]) ).
fof(f3888,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,[],[f3048]) ).
fof(f3910,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,[],[f3088]) ).
fof(f3984,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,[],[f3153]) ).
fof(f4034,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,[],[f3673]) ).
fof(f4035,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,[],[f3673]) ).
fof(f4044,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,[],[f3201]) ).
fof(f4046,plain,
l3_lattices(sK23),
inference(cnf_transformation,[],[f3674]) ).
fof(f4047,plain,
v10_lattices(sK23),
inference(cnf_transformation,[],[f3674]) ).
fof(f4048,plain,
~ v3_struct_0(sK23),
inference(cnf_transformation,[],[f3674]) ).
fof(f4049,plain,
m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23))),
inference(cnf_transformation,[],[f3674]) ).
fof(f4050,plain,
~ v1_xboole_0(sK24),
inference(cnf_transformation,[],[f3674]) ).
fof(f4051,plain,
m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK23))),
inference(cnf_transformation,[],[f3674]) ).
fof(f4052,plain,
~ v1_xboole_0(sK25),
inference(cnf_transformation,[],[f3674]) ).
fof(f4053,plain,
m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23))),
inference(cnf_transformation,[],[f3674]) ).
fof(f4054,plain,
~ v1_xboole_0(sK26),
inference(cnf_transformation,[],[f3674]) ).
fof(f4055,plain,
( r1_tarski(sK25,sK26)
| ~ r1_tarski(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),k19_filter_2(sK23,sK24)) ),
inference(cnf_transformation,[],[f3674]) ).
fof(f4056,plain,
( ~ r1_tarski(k19_filter_2(sK23,sK25),k19_filter_2(sK23,sK26))
| ~ r1_tarski(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),k19_filter_2(sK23,sK24)) ),
inference(cnf_transformation,[],[f3674]) ).
fof(f4077,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,[],[f3216]) ).
fof(f4206,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3328]) ).
fof(f4209,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3332]) ).
fof(f4216,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3332]) ).
fof(f4615,plain,
! [X2,X0,X1] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(cnf_transformation,[],[f3612]) ).
fof(f4617,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f3850]) ).
fof(f4678,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,[],[f4035]) ).
fof(f4679,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,[],[f4034]) ).
fof(f4701,plain,
! [X1] : r1_tarski(X1,X1),
inference(equality_resolution,[],[f4617]) ).
fof(f4734,definition,
( spl142_1
<=> r1_tarski(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),k19_filter_2(sK23,sK24)) ),
introduced(definition,[new_symbols(definition,[spl142_1])],[avatar_definition]) ).
fof(f4735,plain,
( ~ r1_tarski(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),k19_filter_2(sK23,sK24))
| spl142_1 ),
inference(avatar_component_clause,[],[f4734]) ).
fof(f4737,definition,
( spl142_2
<=> r1_tarski(sK25,sK26) ),
introduced(definition,[new_symbols(definition,[spl142_2])],[avatar_definition]) ).
fof(f4738,plain,
( r1_tarski(sK25,sK26)
| ~ spl142_2 ),
inference(avatar_component_clause,[],[f4737]) ).
fof(f4739,plain,
( ~ spl142_1
| spl142_2 ),
inference(avatar_split_clause,[],[f4055,f4737,f4734]) ).
fof(f4741,definition,
( spl142_3
<=> r1_tarski(k19_filter_2(sK23,sK25),k19_filter_2(sK23,sK26)) ),
introduced(definition,[new_symbols(definition,[spl142_3])],[avatar_definition]) ).
fof(f4742,plain,
( ~ r1_tarski(k19_filter_2(sK23,sK25),k19_filter_2(sK23,sK26))
| spl142_3 ),
inference(avatar_component_clause,[],[f4741]) ).
fof(f4743,plain,
( ~ spl142_1
| ~ spl142_3 ),
inference(avatar_split_clause,[],[f4056,f4741,f4734]) ).
fof(f4748,plain,
( sK24 = k7_filter_2(sK23,sK24)
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23) ),
inference(resolution,[],[f4049,f3984]) ).
fof(f4762,plain,
( sK24 = k7_filter_2(sK23,sK24)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23) ),
inference(forward_subsumption_resolution,[],[f4748,f4048]) ).
fof(f4768,plain,
( sK24 = k7_filter_2(sK23,sK24)
| ~ l3_lattices(sK23) ),
inference(forward_subsumption_resolution,[],[f4762,f4047]) ).
fof(f4774,plain,
sK24 = k7_filter_2(sK23,sK24),
inference(forward_subsumption_resolution,[],[f4768,f4046]) ).
fof(f4902,definition,
( spl142_19
<=> m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23))) ),
introduced(definition,[new_symbols(definition,[spl142_19])],[avatar_definition]) ).
fof(f4903,plain,
( ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_19 ),
inference(avatar_component_clause,[],[f4902]) ).
fof(f4905,definition,
( spl142_20
<=> m2_filter_2(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),sK23) ),
introduced(definition,[new_symbols(definition,[spl142_20])],[avatar_definition]) ).
fof(f4906,plain,
( ~ m2_filter_2(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),sK23)
| spl142_20 ),
inference(avatar_component_clause,[],[f4905]) ).
fof(f4908,definition,
( spl142_21
<=> m2_filter_2(k19_filter_2(sK23,sK24),sK23) ),
introduced(definition,[new_symbols(definition,[spl142_21])],[avatar_definition]) ).
fof(f4909,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| spl142_21 ),
inference(avatar_component_clause,[],[f4908]) ).
fof(f4986,plain,
! [X0] :
( k19_filter_2(sK23,sK24) = k3_filter_2(k1_lattice2(sK23),sK24)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| v1_xboole_0(sK24)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23) ),
inference(superposition,[],[f4044,f4774]) ).
fof(f4987,plain,
( m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23))) ),
inference(superposition,[],[f3888,f4774]) ).
fof(f4988,plain,
( m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23))) ),
inference(forward_subsumption_resolution,[],[f4987,f4048]) ).
fof(f4989,plain,
! [X0] :
( k19_filter_2(sK23,sK24) = k3_filter_2(k1_lattice2(sK23),sK24)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23) ),
inference(forward_subsumption_resolution,[],[f4986,f4050]) ).
fof(f4991,plain,
( m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| ~ l3_lattices(sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23))) ),
inference(forward_subsumption_resolution,[],[f4988,f4047]) ).
fof(f4992,plain,
! [X0] :
( k19_filter_2(sK23,sK24) = k3_filter_2(k1_lattice2(sK23),sK24)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23) ),
inference(forward_subsumption_resolution,[],[f4989,f4049]) ).
fof(f4994,plain,
( m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23))) ),
inference(forward_subsumption_resolution,[],[f4991,f4046]) ).
fof(f4995,plain,
! [X0] :
( k19_filter_2(sK23,sK24) = k3_filter_2(k1_lattice2(sK23),sK24)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23) ),
inference(forward_subsumption_resolution,[],[f4992,f4048]) ).
fof(f4997,plain,
m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23)))),
inference(forward_subsumption_resolution,[],[f4994,f4049]) ).
fof(f4998,plain,
! [X0] :
( k19_filter_2(sK23,sK24) = k3_filter_2(k1_lattice2(sK23),sK24)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| ~ l3_lattices(sK23) ),
inference(forward_subsumption_resolution,[],[f4995,f4047]) ).
fof(f5000,plain,
! [X0] :
( k19_filter_2(sK23,sK24) = k3_filter_2(k1_lattice2(sK23),sK24)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23)))) ),
inference(forward_subsumption_resolution,[],[f4998,f4046]) ).
fof(f5003,definition,
( spl142_31
<=> ! [X0] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23)))) ) ),
introduced(definition,[new_symbols(definition,[spl142_31])],[avatar_definition]) ).
fof(f5004,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| v1_xboole_0(X0) )
| ~ spl142_31 ),
inference(avatar_component_clause,[],[f5003]) ).
fof(f5006,definition,
( spl142_32
<=> k19_filter_2(sK23,sK24) = k3_filter_2(k1_lattice2(sK23),sK24) ),
introduced(definition,[new_symbols(definition,[spl142_32])],[avatar_definition]) ).
fof(f5007,plain,
( k19_filter_2(sK23,sK24) = k3_filter_2(k1_lattice2(sK23),sK24)
| ~ spl142_32 ),
inference(avatar_component_clause,[],[f5006]) ).
fof(f5008,plain,
( spl142_31
| spl142_32 ),
inference(avatar_split_clause,[],[f5000,f5006,f5003]) ).
fof(f5123,plain,
( ~ m2_lattice4(k19_filter_2(sK23,sK24),sK23)
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_19 ),
inference(resolution,[],[f4903,f4077]) ).
fof(f5131,plain,
( ~ m2_lattice4(k19_filter_2(sK23,sK24),sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_19 ),
inference(forward_subsumption_resolution,[],[f5123,f4048]) ).
fof(f5134,plain,
( ~ m2_lattice4(k19_filter_2(sK23,sK24),sK23)
| ~ l3_lattices(sK23)
| spl142_19 ),
inference(forward_subsumption_resolution,[],[f5131,f4047]) ).
fof(f5137,plain,
( ~ m2_lattice4(k19_filter_2(sK23,sK24),sK23)
| spl142_19 ),
inference(forward_subsumption_resolution,[],[f5134,f4046]) ).
fof(f5530,plain,
( ~ r1_tarski(sK25,k19_filter_2(sK23,sK26))
| ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| ~ m2_filter_2(k19_filter_2(sK23,sK25),sK23)
| v1_xboole_0(sK25)
| ~ m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_3 ),
inference(resolution,[],[f4742,f4679]) ).
fof(f5532,plain,
( ~ r1_tarski(sK25,k19_filter_2(sK23,sK26))
| ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| v1_xboole_0(sK25)
| ~ m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_3 ),
inference(forward_subsumption_resolution,[],[f5530,f3910]) ).
fof(f5533,plain,
( ~ r1_tarski(sK25,k19_filter_2(sK23,sK26))
| ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| ~ m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_3 ),
inference(forward_subsumption_resolution,[],[f5532,f4052]) ).
fof(f5534,plain,
( ~ r1_tarski(sK25,k19_filter_2(sK23,sK26))
| ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_3 ),
inference(forward_subsumption_resolution,[],[f5533,f4051]) ).
fof(f5535,plain,
( ~ r1_tarski(sK25,k19_filter_2(sK23,sK26))
| ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_3 ),
inference(forward_subsumption_resolution,[],[f5534,f4048]) ).
fof(f5536,plain,
( ~ r1_tarski(sK25,k19_filter_2(sK23,sK26))
| ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| ~ l3_lattices(sK23)
| spl142_3 ),
inference(forward_subsumption_resolution,[],[f5535,f4047]) ).
fof(f5537,plain,
( ~ r1_tarski(sK25,k19_filter_2(sK23,sK26))
| ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| spl142_3 ),
inference(forward_subsumption_resolution,[],[f5536,f4046]) ).
fof(f5539,definition,
( spl142_54
<=> m2_filter_2(k19_filter_2(sK23,sK26),sK23) ),
introduced(definition,[new_symbols(definition,[spl142_54])],[avatar_definition]) ).
fof(f5540,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| spl142_54 ),
inference(avatar_component_clause,[],[f5539]) ).
fof(f5542,definition,
( spl142_55
<=> r1_tarski(sK25,k19_filter_2(sK23,sK26)) ),
introduced(definition,[new_symbols(definition,[spl142_55])],[avatar_definition]) ).
fof(f5543,plain,
( ~ r1_tarski(sK25,k19_filter_2(sK23,sK26))
| spl142_55 ),
inference(avatar_component_clause,[],[f5542]) ).
fof(f5544,plain,
( ~ spl142_54
| ~ spl142_55
| spl142_3 ),
inference(avatar_split_clause,[],[f5537,f4741,f5542,f5539]) ).
fof(f5552,plain,
( v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| v1_xboole_0(sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_54 ),
inference(resolution,[],[f5540,f3910]) ).
fof(f5553,plain,
( ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| v1_xboole_0(sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_54 ),
inference(forward_subsumption_resolution,[],[f5552,f4048]) ).
fof(f5554,plain,
( ~ l3_lattices(sK23)
| v1_xboole_0(sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_54 ),
inference(forward_subsumption_resolution,[],[f5553,f4047]) ).
fof(f5555,plain,
( v1_xboole_0(sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_54 ),
inference(forward_subsumption_resolution,[],[f5554,f4046]) ).
fof(f5556,plain,
( ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_54 ),
inference(forward_subsumption_resolution,[],[f5555,f4054]) ).
fof(f5557,plain,
( $false
| spl142_54 ),
inference(forward_subsumption_resolution,[],[f5556,f4053]) ).
fof(f5558,plain,
spl142_54,
inference(avatar_contradiction_clause,[],[f5557]) ).
fof(f5563,plain,
( ! [X0] :
( ~ r1_tarski(X0,k19_filter_2(sK23,sK26))
| ~ r1_tarski(sK25,X0) )
| spl142_55 ),
inference(resolution,[],[f5543,f4615]) ).
fof(f5640,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_19 ),
inference(resolution,[],[f5137,f3871]) ).
fof(f5643,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_19 ),
inference(forward_subsumption_resolution,[],[f5640,f4048]) ).
fof(f5646,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| ~ l3_lattices(sK23)
| spl142_19 ),
inference(forward_subsumption_resolution,[],[f5643,f4047]) ).
fof(f5649,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| spl142_19 ),
inference(forward_subsumption_resolution,[],[f5646,f4046]) ).
fof(f5651,plain,
( ~ spl142_21
| spl142_19 ),
inference(avatar_split_clause,[],[f5649,f4902,f4908]) ).
fof(f5652,plain,
( v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| v1_xboole_0(sK24)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_21 ),
inference(resolution,[],[f4909,f3910]) ).
fof(f5653,plain,
( ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| v1_xboole_0(sK24)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_21 ),
inference(forward_subsumption_resolution,[],[f5652,f4048]) ).
fof(f5654,plain,
( ~ l3_lattices(sK23)
| v1_xboole_0(sK24)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_21 ),
inference(forward_subsumption_resolution,[],[f5653,f4047]) ).
fof(f5655,plain,
( v1_xboole_0(sK24)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_21 ),
inference(forward_subsumption_resolution,[],[f5654,f4046]) ).
fof(f5656,plain,
( ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_21 ),
inference(forward_subsumption_resolution,[],[f5655,f4050]) ).
fof(f5657,plain,
( $false
| spl142_21 ),
inference(forward_subsumption_resolution,[],[f5656,f4049]) ).
fof(f5658,plain,
spl142_21,
inference(avatar_contradiction_clause,[],[f5657]) ).
fof(f5667,definition,
( spl142_61
<=> v1_xboole_0(k19_filter_2(sK23,sK24)) ),
introduced(definition,[new_symbols(definition,[spl142_61])],[avatar_definition]) ).
fof(f5668,plain,
( v1_xboole_0(k19_filter_2(sK23,sK24))
| ~ spl142_61 ),
inference(avatar_component_clause,[],[f5667]) ).
fof(f5676,plain,
( v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| v1_xboole_0(k19_filter_2(sK23,sK24))
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_20 ),
inference(resolution,[],[f4906,f3910]) ).
fof(f5677,plain,
( ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| v1_xboole_0(k19_filter_2(sK23,sK24))
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_20 ),
inference(forward_subsumption_resolution,[],[f5676,f4048]) ).
fof(f5678,plain,
( ~ l3_lattices(sK23)
| v1_xboole_0(k19_filter_2(sK23,sK24))
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_20 ),
inference(forward_subsumption_resolution,[],[f5677,f4047]) ).
fof(f5679,plain,
( v1_xboole_0(k19_filter_2(sK23,sK24))
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_20 ),
inference(forward_subsumption_resolution,[],[f5678,f4046]) ).
fof(f5680,plain,
( ~ spl142_19
| spl142_61
| spl142_20 ),
inference(avatar_split_clause,[],[f5679,f4905,f5667,f4902]) ).
fof(f5945,definition,
( spl142_77
<=> l3_lattices(k1_lattice2(sK23)) ),
introduced(definition,[new_symbols(definition,[spl142_77])],[avatar_definition]) ).
fof(f5946,plain,
( ~ l3_lattices(k1_lattice2(sK23))
| spl142_77 ),
inference(avatar_component_clause,[],[f5945]) ).
fof(f5948,definition,
( spl142_78
<=> v10_lattices(k1_lattice2(sK23)) ),
introduced(definition,[new_symbols(definition,[spl142_78])],[avatar_definition]) ).
fof(f5949,plain,
( ~ v10_lattices(k1_lattice2(sK23))
| spl142_78 ),
inference(avatar_component_clause,[],[f5948]) ).
fof(f5951,definition,
( spl142_79
<=> v3_struct_0(k1_lattice2(sK23)) ),
introduced(definition,[new_symbols(definition,[spl142_79])],[avatar_definition]) ).
fof(f5952,plain,
( v3_struct_0(k1_lattice2(sK23))
| ~ spl142_79 ),
inference(avatar_component_clause,[],[f5951]) ).
fof(f5998,plain,
( ~ l3_lattices(sK23)
| spl142_77 ),
inference(resolution,[],[f5946,f4206]) ).
fof(f6001,plain,
( $false
| spl142_77 ),
inference(forward_subsumption_resolution,[],[f5998,f4046]) ).
fof(f6002,plain,
spl142_77,
inference(avatar_contradiction_clause,[],[f6001]) ).
fof(f6060,plain,
( v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_78 ),
inference(resolution,[],[f5949,f4209]) ).
fof(f6063,plain,
( ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_78 ),
inference(forward_subsumption_resolution,[],[f6060,f4048]) ).
fof(f6065,plain,
( ~ l3_lattices(sK23)
| spl142_78 ),
inference(forward_subsumption_resolution,[],[f6063,f4047]) ).
fof(f6067,plain,
( $false
| spl142_78 ),
inference(forward_subsumption_resolution,[],[f6065,f4046]) ).
fof(f6068,plain,
spl142_78,
inference(avatar_contradiction_clause,[],[f6067]) ).
fof(f6125,plain,
( v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| ~ spl142_79 ),
inference(resolution,[],[f5952,f4216]) ).
fof(f6128,plain,
( ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| ~ spl142_79 ),
inference(forward_subsumption_resolution,[],[f6125,f4048]) ).
fof(f6131,plain,
( ~ l3_lattices(sK23)
| ~ spl142_79 ),
inference(forward_subsumption_resolution,[],[f6128,f4047]) ).
fof(f6135,plain,
( $false
| ~ spl142_79 ),
inference(forward_subsumption_resolution,[],[f6131,f4046]) ).
fof(f6136,plain,
~ spl142_79,
inference(avatar_contradiction_clause,[],[f6135]) ).
fof(f6203,plain,
( v1_xboole_0(sK24)
| ~ spl142_31 ),
inference(resolution,[],[f5004,f4997]) ).
fof(f6289,plain,
( $false
| ~ spl142_31 ),
inference(forward_subsumption_resolution,[],[f6203,f4050]) ).
fof(f6290,plain,
~ spl142_31,
inference(avatar_contradiction_clause,[],[f6289]) ).
fof(f6322,plain,
( m1_filter_2(k19_filter_2(sK23,sK24),k1_lattice2(sK23))
| v3_struct_0(k1_lattice2(sK23))
| ~ v10_lattices(k1_lattice2(sK23))
| ~ l3_lattices(k1_lattice2(sK23))
| v1_xboole_0(sK24)
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| ~ spl142_32 ),
inference(superposition,[],[f3882,f5007]) ).
fof(f6323,plain,
( m1_filter_2(k19_filter_2(sK23,sK24),k1_lattice2(sK23))
| v3_struct_0(k1_lattice2(sK23))
| ~ v10_lattices(k1_lattice2(sK23))
| ~ l3_lattices(k1_lattice2(sK23))
| ~ m1_subset_1(sK24,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK23))))
| ~ spl142_32 ),
inference(forward_subsumption_resolution,[],[f6322,f4050]) ).
fof(f6326,plain,
( m1_filter_2(k19_filter_2(sK23,sK24),k1_lattice2(sK23))
| v3_struct_0(k1_lattice2(sK23))
| ~ v10_lattices(k1_lattice2(sK23))
| ~ l3_lattices(k1_lattice2(sK23))
| ~ spl142_32 ),
inference(forward_subsumption_resolution,[],[f6323,f4997]) ).
fof(f6330,definition,
( spl142_113
<=> m1_filter_2(k19_filter_2(sK23,sK24),k1_lattice2(sK23)) ),
introduced(definition,[new_symbols(definition,[spl142_113])],[avatar_definition]) ).
fof(f6331,plain,
( m1_filter_2(k19_filter_2(sK23,sK24),k1_lattice2(sK23))
| ~ spl142_113 ),
inference(avatar_component_clause,[],[f6330]) ).
fof(f6332,plain,
( ~ spl142_77
| ~ spl142_78
| spl142_79
| spl142_113
| ~ spl142_32 ),
inference(avatar_split_clause,[],[f6326,f5006,f6330,f5951,f5948,f5945]) ).
fof(f6518,plain,
( ~ r1_tarski(sK25,sK26)
| ~ m2_filter_2(k19_filter_2(sK23,sK26),sK23)
| v1_xboole_0(sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_55 ),
inference(resolution,[],[f5563,f4678]) ).
fof(f6528,plain,
( ~ r1_tarski(sK25,sK26)
| v1_xboole_0(sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_55 ),
inference(forward_subsumption_resolution,[],[f6518,f3910]) ).
fof(f6529,plain,
( v1_xboole_0(sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| ~ spl142_2
| spl142_55 ),
inference(forward_subsumption_resolution,[],[f6528,f4738]) ).
fof(f6530,plain,
( ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| ~ spl142_2
| spl142_55 ),
inference(forward_subsumption_resolution,[],[f6529,f4054]) ).
fof(f6531,plain,
( v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| ~ spl142_2
| spl142_55 ),
inference(forward_subsumption_resolution,[],[f6530,f4053]) ).
fof(f6532,plain,
( ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| ~ spl142_2
| spl142_55 ),
inference(forward_subsumption_resolution,[],[f6531,f4048]) ).
fof(f6533,plain,
( ~ l3_lattices(sK23)
| ~ spl142_2
| spl142_55 ),
inference(forward_subsumption_resolution,[],[f6532,f4047]) ).
fof(f6534,plain,
( $false
| ~ spl142_2
| spl142_55 ),
inference(forward_subsumption_resolution,[],[f6533,f4046]) ).
fof(f6535,plain,
( ~ spl142_2
| spl142_55 ),
inference(avatar_contradiction_clause,[],[f6534]) ).
fof(f6536,plain,
( ~ r1_tarski(k19_filter_2(sK23,sK24),k19_filter_2(sK23,sK24))
| ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| ~ m2_filter_2(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),sK23)
| v1_xboole_0(k19_filter_2(sK23,sK24))
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_1 ),
inference(resolution,[],[f4735,f4679]) ).
fof(f6538,plain,
( ~ r1_tarski(k19_filter_2(sK23,sK24),k19_filter_2(sK23,sK24))
| ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| ~ m2_filter_2(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),sK23)
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_1 ),
inference(forward_subsumption_resolution,[],[f6536,f3872]) ).
fof(f6539,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| ~ m2_filter_2(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),sK23)
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| v3_struct_0(sK23)
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_1 ),
inference(forward_subsumption_resolution,[],[f6538,f4701]) ).
fof(f6540,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| ~ m2_filter_2(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),sK23)
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| ~ v10_lattices(sK23)
| ~ l3_lattices(sK23)
| spl142_1 ),
inference(forward_subsumption_resolution,[],[f6539,f4048]) ).
fof(f6541,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| ~ m2_filter_2(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),sK23)
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| ~ l3_lattices(sK23)
| spl142_1 ),
inference(forward_subsumption_resolution,[],[f6540,f4047]) ).
fof(f6542,plain,
( ~ m2_filter_2(k19_filter_2(sK23,sK24),sK23)
| ~ m2_filter_2(k19_filter_2(sK23,k19_filter_2(sK23,sK24)),sK23)
| ~ m1_subset_1(k19_filter_2(sK23,sK24),k1_zfmisc_1(u1_struct_0(sK23)))
| spl142_1 ),
inference(forward_subsumption_resolution,[],[f6541,f4046]) ).
fof(f6543,plain,
( ~ spl142_19
| ~ spl142_20
| ~ spl142_21
| spl142_1 ),
inference(avatar_split_clause,[],[f6542,f4734,f4908,f4905,f4902]) ).
fof(f9079,plain,
( ~ v1_xboole_0(k19_filter_2(sK23,sK24))
| v3_struct_0(k1_lattice2(sK23))
| ~ v10_lattices(k1_lattice2(sK23))
| ~ l3_lattices(k1_lattice2(sK23))
| ~ spl142_113 ),
inference(resolution,[],[f6331,f3867]) ).
fof(f9080,plain,
( v3_struct_0(k1_lattice2(sK23))
| ~ v10_lattices(k1_lattice2(sK23))
| ~ l3_lattices(k1_lattice2(sK23))
| ~ spl142_61
| ~ spl142_113 ),
inference(forward_subsumption_resolution,[],[f9079,f5668]) ).
fof(f9082,plain,
( ~ spl142_77
| ~ spl142_78
| spl142_79
| ~ spl142_61
| ~ spl142_113 ),
inference(avatar_split_clause,[],[f9080,f6330,f5667,f5951,f5948,f5945]) ).
cnf(s1,plain,
( ~ spl142_1
| spl142_2 ),
inference(sat_conversion,[],[f4739]) ).
cnf(s2,plain,
( ~ spl142_1
| ~ spl142_3 ),
inference(sat_conversion,[],[f4743]) ).
cnf(s17,plain,
( spl142_31
| spl142_32 ),
inference(sat_conversion,[],[f5008]) ).
cnf(s35,plain,
( spl142_3
| ~ spl142_54
| ~ spl142_55 ),
inference(sat_conversion,[],[f5544]) ).
cnf(s36,plain,
spl142_54,
inference(sat_conversion,[],[f5558]) ).
cnf(s45,plain,
( spl142_19
| ~ spl142_21 ),
inference(sat_conversion,[],[f5651]) ).
cnf(s46,plain,
spl142_21,
inference(sat_conversion,[],[f5658]) ).
cnf(s49,plain,
( ~ spl142_19
| spl142_20
| spl142_61 ),
inference(sat_conversion,[],[f5680]) ).
cnf(s80,plain,
spl142_77,
inference(sat_conversion,[],[f6002]) ).
cnf(s88,plain,
spl142_78,
inference(sat_conversion,[],[f6068]) ).
cnf(s97,plain,
~ spl142_79,
inference(sat_conversion,[],[f6136]) ).
cnf(s104,plain,
~ spl142_31,
inference(sat_conversion,[],[f6290]) ).
cnf(s112,plain,
( ~ spl142_32
| ~ spl142_77
| ~ spl142_78
| spl142_79
| spl142_113 ),
inference(sat_conversion,[],[f6332]) ).
cnf(s135,plain,
( ~ spl142_2
| spl142_55 ),
inference(sat_conversion,[],[f6535]) ).
cnf(s136,plain,
( spl142_1
| ~ spl142_19
| ~ spl142_20
| ~ spl142_21 ),
inference(sat_conversion,[],[f6543]) ).
cnf(s224,plain,
( ~ spl142_61
| ~ spl142_77
| ~ spl142_78
| spl142_79
| ~ spl142_113 ),
inference(sat_conversion,[],[f9082]) ).
cnf(s264,plain,
spl142_19,
inference(rat,[],[s45,s46]) ).
cnf(s265,plain,
( spl142_3
| ~ spl142_55 ),
inference(rat,[],[s35,s36]) ).
cnf(s284,plain,
spl142_32,
inference(rat,[],[s17,s104]) ).
cnf(s286,plain,
spl142_113,
inference(rat,[],[s112,s80,s97,s88,s284]) ).
cnf(s287,plain,
~ spl142_61,
inference(rat,[],[s224,s80,s97,s88,s286]) ).
cnf(s288,plain,
spl142_20,
inference(rat,[],[s49,s264,s287]) ).
cnf(s289,plain,
spl142_1,
inference(rat,[],[s136,s46,s264,s288]) ).
cnf(s290,plain,
~ spl142_3,
inference(rat,[],[s2,s289]) ).
cnf(s291,plain,
~ spl142_55,
inference(rat,[],[s265,s290]) ).
cnf(s292,plain,
~ spl142_2,
inference(rat,[],[s135,s291]) ).
cnf(s293,plain,
$false,
inference(rat,[],[s1,s292,s289]) ).
fof(f9085,plain,
$false,
inference(avatar_sat_refutation,[],[s293]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT310+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n006.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 14:27:56 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.67/2.45 % (3036218)Detected formulas, will run a generic FOF schedule.
% 10.67/2.45 % (3036224)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=1039419838:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 10.67/2.45 % (3036225)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=3738160171:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 10.67/2.45 % (3036223)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=3935847959:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 10.67/2.45 % (3036227)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=459830763:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 10.67/2.45 % (3036229)dis-21_1_sil=8000:lcm=predicate:random_seed=3092162829:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 10.67/2.45 % (3036226)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=199498256:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 10.67/2.45 % (3036228)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1616019204:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 10.67/2.45 % (3036226)Instruction limit reached!
% 10.67/2.45 % (3036226)------------------------------
% 10.67/2.45 % (3036226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036226)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036226)Termination reason: Instruction limit
% 10.67/2.45 % (3036226)Termination phase: Saturation
% 10.67/2.45 % (3036226)Time elapsed: 0.072 s
% 10.67/2.45 % (3036226)Peak memory usage: 92 MB
% 10.67/2.45 % (3036226)Instructions burned: 109 (million)
% 10.67/2.45 % (3036229)Instruction limit reached!
% 10.67/2.45 % (3036229)------------------------------
% 10.67/2.45 % (3036229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036229)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036229)Termination reason: Instruction limit
% 10.67/2.45 % (3036229)Termination phase: Property scanning
% 10.67/2.45 % (3036229)Time elapsed: 0.075 s
% 10.67/2.45 % (3036229)Peak memory usage: 93 MB
% 10.67/2.45 % (3036229)Instructions burned: 129 (million)
% 10.67/2.45 % (3036227)Instruction limit reached!
% 10.67/2.45 % (3036227)------------------------------
% 10.67/2.45 % (3036227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036227)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036227)Termination reason: Instruction limit
% 10.67/2.45 % (3036227)Termination phase: Saturation
% 10.67/2.45 % (3036227)Time elapsed: 0.077 s
% 10.67/2.45 % (3036227)Peak memory usage: 92 MB
% 10.67/2.45 % (3036227)Instructions burned: 119 (million)
% 10.67/2.45 % (3036228)Instruction limit reached!
% 10.67/2.45 % (3036228)------------------------------
% 10.67/2.45 % (3036228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036228)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036228)Termination reason: Instruction limit
% 10.67/2.45 % (3036228)Termination phase: Property scanning
% 10.67/2.45 % (3036228)Time elapsed: 0.085 s
% 10.67/2.45 % (3036228)Peak memory usage: 94 MB
% 10.67/2.45 % (3036228)Instructions burned: 139 (million)
% 10.67/2.45 % (3036237)lrs+10_1_sil=8000:sp=occurrence:random_seed=2752851193:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 10.67/2.45 % (3036238)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3594115388:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.67/2.45 % (3036239)lrs+1011_1_sil=32000:sp=occurrence:random_seed=495138521:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 10.67/2.45 % (3036240)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=3027505794:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 10.67/2.45 % (3036238)Instruction limit reached!
% 10.67/2.45 % (3036238)------------------------------
% 10.67/2.45 % (3036238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036238)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036238)Termination reason: Instruction limit
% 10.67/2.45 % (3036238)Termination phase: Saturation
% 10.67/2.45 % (3036238)Time elapsed: 0.088 s
% 10.67/2.45 % (3036238)Peak memory usage: 93 MB
% 10.67/2.45 % (3036238)Instructions burned: 157 (million)
% 10.67/2.45 % (3036240)Instruction limit reached!
% 10.67/2.45 % (3036240)------------------------------
% 10.67/2.45 % (3036240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036240)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036240)Termination reason: Instruction limit
% 10.67/2.45 % (3036240)Termination phase: Saturation
% 10.67/2.45 % (3036240)Time elapsed: 0.135 s
% 10.67/2.45 % (3036240)Peak memory usage: 98 MB
% 10.67/2.45 % (3036240)Instructions burned: 249 (million)
% 10.67/2.45 % (3036237)Instruction limit reached!
% 10.67/2.45 % (3036237)------------------------------
% 10.67/2.45 % (3036237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036237)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036237)Termination reason: Instruction limit
% 10.67/2.45 % (3036237)Termination phase: Saturation
% 10.67/2.45 % (3036237)Time elapsed: 0.175 s
% 10.67/2.45 % (3036237)Peak memory usage: 95 MB
% 10.67/2.45 % (3036237)Instructions burned: 286 (million)
% 10.67/2.45 % (3036239)Instruction limit reached!
% 10.67/2.45 % (3036239)------------------------------
% 10.67/2.45 % (3036239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036239)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036239)Termination reason: Instruction limit
% 10.67/2.45 % (3036239)Termination phase: Saturation
% 10.67/2.45 % (3036239)Time elapsed: 0.211 s
% 10.67/2.45 % (3036239)Peak memory usage: 93 MB
% 10.67/2.45 % (3036239)Instructions burned: 325 (million)
% 10.67/2.45 % (3036245)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1118647518:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 10.67/2.45 % (3036246)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3024641063:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 10.67/2.45 % (3036247)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2669347660:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 10.67/2.45 % (3036248)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=386199299:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 10.67/2.45 % (3036247)Instruction limit reached!
% 10.67/2.45 % (3036247)------------------------------
% 10.67/2.45 % (3036247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036247)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036247)Termination reason: Instruction limit
% 10.67/2.45 % (3036247)Termination phase: Saturation
% 10.67/2.45 % (3036247)Time elapsed: 0.066 s
% 10.67/2.45 % (3036247)Peak memory usage: 93 MB
% 10.67/2.45 % (3036247)Instructions burned: 115 (million)
% 10.67/2.45 % (3036245)Instruction limit reached!
% 10.67/2.45 % (3036245)------------------------------
% 10.67/2.45 % (3036245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036245)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036245)Termination reason: Instruction limit
% 10.67/2.45 % (3036245)Termination phase: Saturation
% 10.67/2.45 % (3036245)Time elapsed: 0.167 s
% 10.67/2.45 % (3036245)Peak memory usage: 95 MB
% 10.67/2.45 % (3036245)Instructions burned: 294 (million)
% 10.67/2.45 % (3036248)Instruction limit reached!
% 10.67/2.45 % (3036248)------------------------------
% 10.67/2.45 % (3036248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036248)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036248)Termination reason: Instruction limit
% 10.67/2.45 % (3036248)Termination phase: Property scanning
% 10.67/2.45 % (3036248)Time elapsed: 0.075 s
% 10.67/2.45 % (3036248)Peak memory usage: 94 MB
% 10.67/2.45 % (3036248)Instructions burned: 129 (million)
% 10.67/2.45 % (3036254)lrs+10_1_sil=8000:sp=occurrence:random_seed=3505095585:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 10.67/2.45 % (3036253)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3975360760:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 10.67/2.45 % (3036253)Instruction limit reached!
% 10.67/2.45 % (3036253)------------------------------
% 10.67/2.45 % (3036253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.45 % (3036253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.45 % (3036253)CaDiCaL version: 2.1.3
% 10.67/2.45 % (3036253)Termination reason: Instruction limit
% 10.67/2.45 % (3036253)Termination phase: Property scanning
% 10.67/2.45 % (3036253)Time elapsed: 0.057 s
% 10.67/2.45 % (3036253)Peak memory usage: 91 MB
% 10.67/2.45 % (3036253)Instructions burned: 114 (million)
% 10.67/2.45 % (3036255)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3051240095:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 10.67/2.45 % (3036258)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1668853008:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 10.67/2.45 % (3036255)First to succeed.
% 10.67/2.45 % (3036255)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3036218"
% 10.67/2.45 % (3036224)Also succeeded, but the first one will report.
% 10.67/2.45 % (3036255)Refutation found. Thanks to Tanya!
% 10.67/2.45 % SZS status Theorem for theBenchmark
% 10.67/2.45 % SZS output start Proof for theBenchmark
% See solution above
% 11.08/2.54 % (3036255)------------------------------
% 11.08/2.54 % (3036255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.08/2.54 % (3036255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.08/2.54 % (3036255)CaDiCaL version: 2.1.3
% 11.08/2.54 % (3036255)Termination reason: Refutation
% 11.08/2.54 % (3036255)Time elapsed: 0.192 s
% 11.08/2.54 % (3036255)Peak memory usage: 96 MB
% 11.08/2.54 % (3036255)Instructions burned: 335 (million)
% 11.08/2.54 % (3036255)------------------------------
% 11.08/2.54 % (3036255)------------------------------
% 11.08/2.54 % (3036218)Success in time 1.595 s
% 11.08/2.54 % Vampire exiting
%------------------------------------------------------------------------------