%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT312+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 : n009.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:48 AM UTC 2026
% Result : Theorem 42.71s 9.52s
% Output : Refutation 53.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 38
% Syntax : Number of formulae : 304 ( 47 unt; 13 def)
% Number of atoms : 1221 ( 168 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 1497 ( 580 ~; 694 |; 151 &)
% ( 25 <=>; 47 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 14 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 3 con; 0-3 aty)
% Number of variables : 320 ( 1 sgn 311 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f2211,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_domain_1) ).
fof(f8588,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f8589,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_0(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f8606,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( X2 = k6_domain_1(u1_struct_0(X0),X1)
=> k3_filter_0(X0,X2) = k2_filter_0(X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_filter_0) ).
fof(f8673,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f9358,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(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(f9391,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(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(f13532,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f13533,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(f13537,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f13541,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k2_filter_2(X0,X1) = k2_filter_0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f13543,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))) )
=> k3_filter_2(X0,X1) = k3_filter_0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k3_filter_2) ).
fof(f13567,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m2_filter_2(k18_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k18_filter_2) ).
fof(f13596,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f13601,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f13602,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(f13614,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_filter_2) ).
fof(f13616,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_filter_2) ).
fof(f13624,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(f13626,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,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t38_filter_2) ).
fof(f13630,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t41_filter_2) ).
fof(f13631,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13630]) ).
fof(f13636,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f13680,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13532]) ).
fof(f13681,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13680]) ).
fof(f13682,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,[],[f13533]) ).
fof(f13683,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,[],[f13682]) ).
fof(f13690,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f13537]) ).
fof(f13691,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f13690]) ).
fof(f13698,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f13541]) ).
fof(f13699,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13698]) ).
fof(f13702,plain,
! [X0,X1] :
( k3_filter_2(X0,X1) = k3_filter_0(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))) ),
inference(ennf_transformation,[],[f13543]) ).
fof(f13703,plain,
! [X0,X1] :
( k3_filter_2(X0,X1) = k3_filter_0(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))) ),
inference(flattening,[],[f13702]) ).
fof(f13750,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f13567]) ).
fof(f13751,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13750]) ).
fof(f13805,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13596]) ).
fof(f13806,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13805]) ).
fof(f13815,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13601]) ).
fof(f13816,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13815]) ).
fof(f13817,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,[],[f13602]) ).
fof(f13818,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,[],[f13817]) ).
fof(f13841,plain,
! [X0] :
( ! [X1] :
( k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13614]) ).
fof(f13842,plain,
! [X0] :
( ! [X1] :
( k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13841]) ).
fof(f13845,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13616]) ).
fof(f13846,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13845]) ).
fof(f13861,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,[],[f13624]) ).
fof(f13862,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,[],[f13861]) ).
fof(f13865,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,[],[f13626]) ).
fof(f13866,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,[],[f13865]) ).
fof(f13867,plain,
! [X0] :
( ! [X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13627]) ).
fof(f13868,plain,
! [X0] :
( ! [X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13867]) ).
fof(f13873,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1))
& r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13631]) ).
fof(f13874,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1))
& r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f13873]) ).
fof(f13907,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8673]) ).
fof(f13908,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13907]) ).
fof(f13909,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8588]) ).
fof(f13910,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13909]) ).
fof(f13935,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8589]) ).
fof(f13936,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13935]) ).
fof(f13953,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_filter_0(X0,X2) = k2_filter_0(X0,X1)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8606]) ).
fof(f13954,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_filter_0(X0,X2) = k2_filter_0(X0,X1)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13953]) ).
fof(f14001,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9391]) ).
fof(f14002,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14001]) ).
fof(f14014,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f14017,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9363]) ).
fof(f14018,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14017]) ).
fof(f14019,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f14020,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14019]) ).
fof(f14337,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f2211]) ).
fof(f14338,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f14337]) ).
fof(f18206,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13681]) ).
fof(f18208,plain,
! [X0,X1,X2] :
( ( ( r1_filter_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_filter_2(X0,X1,X2) ) )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f13691]) ).
fof(f18226,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13816]) ).
fof(f18243,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,[],[f13862]) ).
fof(f18244,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,[],[f18243]) ).
fof(f18245,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,[],[f18244]) ).
fof(f18246,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK38(X0,X1,X2))
& r1_tarski(X1,sK38(X0,X1,X2))
& m2_filter_2(sK38(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,[sK38]),skolemize(X3,sK38(X0,X1,X2))],[f18245]) ).
fof(f18247,plain,
( ~ r1_filter_2(u1_struct_0(sK39),k19_filter_2(sK39,sK41),k18_filter_2(sK39,sK40))
& r1_filter_2(u1_struct_0(sK39),sK41,k6_domain_1(u1_struct_0(sK39),sK40))
& ~ v1_xboole_0(sK41)
& m1_subset_1(sK41,k1_zfmisc_1(u1_struct_0(sK39)))
& m1_subset_1(sK40,u1_struct_0(sK39))
& ~ v3_struct_0(sK39)
& v10_lattices(sK39)
& l3_lattices(sK39) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39,sK40,sK41]),skolemize(X0,sK39),skolemize(X1,sK40),skolemize(X2,sK41)],[f13874]) ).
fof(f19689,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18206]) ).
fof(f19692,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13683]) ).
fof(f19696,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ r1_filter_2(X0,X1,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| X1 = X2 ),
inference(cnf_transformation,[],[f18208]) ).
fof(f19701,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| k2_filter_0(X0,X1) = k2_filter_2(X0,X1)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13699]) ).
fof(f19703,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| k3_filter_0(X0,X1) = k3_filter_2(X0,X1)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f13703]) ).
fof(f19729,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13751]) ).
fof(f19790,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k5_filter_2(X0,X1) = X1
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13806]) ).
fof(f19802,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18226]) ).
fof(f19804,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| k7_filter_2(X0,X1) = X1
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13818]) ).
fof(f19830,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13842]) ).
fof(f19834,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13846]) ).
fof(f19857,plain,
! [X2,X0,X1] :
( r1_tarski(X1,sK38(X0,X1,X2))
| ~ 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,[],[f18246]) ).
fof(f19858,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X2,sK38(X0,X1,X2))
| ~ 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,[],[f18246]) ).
fof(f19864,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| 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)
| k19_filter_2(X0,X1) = k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13866]) ).
fof(f19865,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13868]) ).
fof(f19869,plain,
l3_lattices(sK39),
inference(cnf_transformation,[],[f18247]) ).
fof(f19870,plain,
v10_lattices(sK39),
inference(cnf_transformation,[],[f18247]) ).
fof(f19871,plain,
~ v3_struct_0(sK39),
inference(cnf_transformation,[],[f18247]) ).
fof(f19872,plain,
m1_subset_1(sK40,u1_struct_0(sK39)),
inference(cnf_transformation,[],[f18247]) ).
fof(f19873,plain,
m1_subset_1(sK41,k1_zfmisc_1(u1_struct_0(sK39))),
inference(cnf_transformation,[],[f18247]) ).
fof(f19874,plain,
~ v1_xboole_0(sK41),
inference(cnf_transformation,[],[f18247]) ).
fof(f19875,plain,
r1_filter_2(u1_struct_0(sK39),sK41,k6_domain_1(u1_struct_0(sK39),sK40)),
inference(cnf_transformation,[],[f18247]) ).
fof(f19876,plain,
~ r1_filter_2(u1_struct_0(sK39),k19_filter_2(sK39,sK41),k18_filter_2(sK39,sK40)),
inference(cnf_transformation,[],[f18247]) ).
fof(f19920,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13908]) ).
fof(f19921,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13908]) ).
fof(f19922,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(u1_struct_0(X0),X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13910]) ).
fof(f19945,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13936]) ).
fof(f19958,plain,
! [X2,X0,X1] :
( k2_filter_0(X0,X1) = k3_filter_0(X0,X2)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13954]) ).
fof(f20008,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f14002]) ).
fof(f20030,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f14014]) ).
fof(f20033,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14018]) ).
fof(f20043,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14020]) ).
fof(f20519,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f14338]) ).
fof(f20550,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f13636]) ).
fof(f27112,plain,
! [X0,X1] :
( ~ m1_subset_1(k6_domain_1(u1_struct_0(X0),X1),k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(k6_domain_1(u1_struct_0(X0),X1))
| k2_filter_0(X0,X1) = k3_filter_0(X0,k6_domain_1(u1_struct_0(X0),X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f19958]) ).
fof(f28601,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| v3_struct_0(sK39)
| r1_filter_2(u1_struct_0(sK39),k19_filter_2(sK39,X0),X0)
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f19870,f19865]) ).
fof(f28602,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| r1_filter_2(u1_struct_0(sK39),k19_filter_2(sK39,X0),X0)
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f28601,f19871]) ).
fof(f28603,plain,
! [X0] :
( r1_filter_2(u1_struct_0(sK39),k19_filter_2(sK39,X0),X0)
| ~ m2_filter_2(X0,sK39) ),
inference(forward_subsumption_resolution,[],[f28602,f19869]) ).
fof(f28619,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| v3_struct_0(sK39)
| k18_filter_2(sK39,X0) = k2_filter_2(k1_lattice2(sK39),k5_filter_2(sK39,X0))
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f19834,f19870]) ).
fof(f28620,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| k18_filter_2(sK39,X0) = k2_filter_2(k1_lattice2(sK39),k5_filter_2(sK39,X0))
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f28619,f19871]) ).
fof(f28621,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| k18_filter_2(sK39,X0) = k2_filter_2(k1_lattice2(sK39),k5_filter_2(sK39,X0)) ),
inference(forward_subsumption_resolution,[],[f28620,f19869]) ).
fof(f28622,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| v3_struct_0(sK39)
| k18_filter_2(sK39,X0) = a_2_0_filter_2(sK39,X0)
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f19830,f19870]) ).
fof(f28623,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| k18_filter_2(sK39,X0) = a_2_0_filter_2(sK39,X0)
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f28622,f19871]) ).
fof(f28624,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| k18_filter_2(sK39,X0) = a_2_0_filter_2(sK39,X0) ),
inference(forward_subsumption_resolution,[],[f28623,f19869]) ).
fof(f28628,plain,
k18_filter_2(sK39,sK40) = k2_filter_2(k1_lattice2(sK39),k5_filter_2(sK39,sK40)),
inference(resolution,[],[f28621,f19872]) ).
fof(f28629,plain,
! [X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39))))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK39)))
| v3_struct_0(sK39)
| k19_filter_2(sK39,X1) = k3_filter_2(k1_lattice2(sK39),k7_filter_2(sK39,X1))
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f19864,f19870]) ).
fof(f28630,plain,
! [X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39))))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK39)))
| k19_filter_2(sK39,X1) = k3_filter_2(k1_lattice2(sK39),k7_filter_2(sK39,X1))
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f28629,f19871]) ).
fof(f28631,plain,
! [X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39))))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK39)))
| k19_filter_2(sK39,X1) = k3_filter_2(k1_lattice2(sK39),k7_filter_2(sK39,X1)) ),
inference(forward_subsumption_resolution,[],[f28630,f19869]) ).
fof(f28633,definition,
( spl869_43
<=> ! [X1] :
( v1_xboole_0(X1)
| k19_filter_2(sK39,X1) = k3_filter_2(k1_lattice2(sK39),k7_filter_2(sK39,X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK39))) ) ),
introduced(definition,[new_symbols(definition,[spl869_43])],[avatar_definition]) ).
fof(f28634,plain,
( ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK39)))
| k19_filter_2(sK39,X1) = k3_filter_2(k1_lattice2(sK39),k7_filter_2(sK39,X1))
| v1_xboole_0(X1) )
| ~ spl869_43 ),
inference(avatar_component_clause,[],[f28633]) ).
fof(f28636,definition,
( spl869_44
<=> ! [X0] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39)))) ) ),
introduced(definition,[new_symbols(definition,[spl869_44])],[avatar_definition]) ).
fof(f28637,plain,
( ! [X0] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39)))) )
| ~ spl869_44 ),
inference(avatar_component_clause,[],[f28636]) ).
fof(f28638,plain,
( spl869_43
| spl869_44 ),
inference(avatar_split_clause,[],[f28631,f28636,f28633]) ).
fof(f28639,plain,
( k19_filter_2(sK39,sK41) = k3_filter_2(k1_lattice2(sK39),k7_filter_2(sK39,sK41))
| v1_xboole_0(sK41)
| ~ spl869_43 ),
inference(resolution,[],[f28634,f19873]) ).
fof(f28641,plain,
( k19_filter_2(sK39,sK41) = k3_filter_2(k1_lattice2(sK39),k7_filter_2(sK39,sK41))
| ~ spl869_43 ),
inference(forward_subsumption_resolution,[],[f28639,f19874]) ).
fof(f28642,plain,
k18_filter_2(sK39,sK40) = a_2_0_filter_2(sK39,sK40),
inference(resolution,[],[f28624,f19872]) ).
fof(f28646,plain,
( m2_filter_2(a_2_0_filter_2(sK39,sK40),sK39)
| v3_struct_0(sK39)
| ~ v10_lattices(sK39)
| ~ l3_lattices(sK39)
| ~ m1_subset_1(sK40,u1_struct_0(sK39)) ),
inference(superposition,[],[f19729,f28642]) ).
fof(f28647,plain,
( m2_filter_2(a_2_0_filter_2(sK39,sK40),sK39)
| ~ v10_lattices(sK39)
| ~ l3_lattices(sK39)
| ~ m1_subset_1(sK40,u1_struct_0(sK39)) ),
inference(forward_subsumption_resolution,[],[f28646,f19871]) ).
fof(f28649,plain,
( m2_filter_2(a_2_0_filter_2(sK39,sK40),sK39)
| ~ l3_lattices(sK39)
| ~ m1_subset_1(sK40,u1_struct_0(sK39)) ),
inference(forward_subsumption_resolution,[],[f28647,f19870]) ).
fof(f28650,plain,
( m2_filter_2(a_2_0_filter_2(sK39,sK40),sK39)
| ~ m1_subset_1(sK40,u1_struct_0(sK39)) ),
inference(forward_subsumption_resolution,[],[f28649,f19869]) ).
fof(f28651,plain,
m2_filter_2(a_2_0_filter_2(sK39,sK40),sK39),
inference(forward_subsumption_resolution,[],[f28650,f19872]) ).
fof(f28659,plain,
! [X2,X0,X1] :
( ~ r1_filter_2(X0,X1,k6_domain_1(X0,X2))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k6_domain_1(X0,X2) = X1
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,X0) ),
inference(resolution,[],[f19696,f20519]) ).
fof(f28660,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ r1_filter_2(X0,X1,k6_domain_1(X0,X2))
| k6_domain_1(X0,X2) = X1
| ~ m1_subset_1(X2,X0) ),
inference(duplicate_literal_removal,[],[f28659]) ).
fof(f28670,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| v3_struct_0(sK39)
| k7_filter_2(sK39,X0) = X0
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f19804,f19870]) ).
fof(f28671,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| k7_filter_2(sK39,X0) = X0
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f28670,f19871]) ).
fof(f28672,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| k7_filter_2(sK39,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f28671,f19869]) ).
fof(f28687,plain,
( v3_struct_0(sK39)
| u1_struct_0(sK39) = u1_struct_0(k1_lattice2(sK39)) ),
inference(resolution,[],[f20008,f19869]) ).
fof(f28688,plain,
u1_struct_0(sK39) = u1_struct_0(k1_lattice2(sK39)),
inference(forward_subsumption_resolution,[],[f28687,f19871]) ).
fof(f28690,plain,
! [X0] :
( ~ m1_subset_1(k6_domain_1(u1_struct_0(sK39),X0),k1_zfmisc_1(u1_struct_0(sK39)))
| v1_xboole_0(k6_domain_1(u1_struct_0(sK39),X0))
| k2_filter_0(k1_lattice2(sK39),X0) = k3_filter_0(k1_lattice2(sK39),k6_domain_1(u1_struct_0(sK39),X0))
| ~ m1_subset_1(X0,u1_struct_0(sK39))
| v3_struct_0(k1_lattice2(sK39))
| ~ v10_lattices(k1_lattice2(sK39))
| ~ l3_lattices(k1_lattice2(sK39)) ),
inference(superposition,[],[f27112,f28688]) ).
fof(f28692,definition,
( spl869_45
<=> l3_lattices(k1_lattice2(sK39)) ),
introduced(definition,[new_symbols(definition,[spl869_45])],[avatar_definition]) ).
fof(f28693,plain,
( ~ l3_lattices(k1_lattice2(sK39))
| spl869_45 ),
inference(avatar_component_clause,[],[f28692]) ).
fof(f28695,definition,
( spl869_46
<=> v10_lattices(k1_lattice2(sK39)) ),
introduced(definition,[new_symbols(definition,[spl869_46])],[avatar_definition]) ).
fof(f28696,plain,
( ~ v10_lattices(k1_lattice2(sK39))
| spl869_46 ),
inference(avatar_component_clause,[],[f28695]) ).
fof(f28698,definition,
( spl869_47
<=> v3_struct_0(k1_lattice2(sK39)) ),
introduced(definition,[new_symbols(definition,[spl869_47])],[avatar_definition]) ).
fof(f28699,plain,
( v3_struct_0(k1_lattice2(sK39))
| ~ spl869_47 ),
inference(avatar_component_clause,[],[f28698]) ).
fof(f28701,definition,
( spl869_48
<=> ! [X0] :
( ~ m1_subset_1(k6_domain_1(u1_struct_0(sK39),X0),k1_zfmisc_1(u1_struct_0(sK39)))
| ~ m1_subset_1(X0,u1_struct_0(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k3_filter_0(k1_lattice2(sK39),k6_domain_1(u1_struct_0(sK39),X0))
| v1_xboole_0(k6_domain_1(u1_struct_0(sK39),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl869_48])],[avatar_definition]) ).
fof(f28702,plain,
( ! [X0] :
( ~ m1_subset_1(k6_domain_1(u1_struct_0(sK39),X0),k1_zfmisc_1(u1_struct_0(sK39)))
| ~ m1_subset_1(X0,u1_struct_0(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k3_filter_0(k1_lattice2(sK39),k6_domain_1(u1_struct_0(sK39),X0))
| v1_xboole_0(k6_domain_1(u1_struct_0(sK39),X0)) )
| ~ spl869_48 ),
inference(avatar_component_clause,[],[f28701]) ).
fof(f28703,plain,
( ~ spl869_45
| ~ spl869_46
| spl869_47
| spl869_48 ),
inference(avatar_split_clause,[],[f28690,f28701,f28698,f28695,f28692]) ).
fof(f28711,plain,
( v3_struct_0(sK39)
| u1_struct_0(sK39) = k1_filter_0(sK39)
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f19945,f19870]) ).
fof(f28712,plain,
( u1_struct_0(sK39) = k1_filter_0(sK39)
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f28711,f19871]) ).
fof(f28713,plain,
u1_struct_0(sK39) = k1_filter_0(sK39),
inference(forward_subsumption_resolution,[],[f28712,f19869]) ).
fof(f28714,plain,
m1_subset_1(sK40,k1_filter_0(sK39)),
inference(superposition,[],[f19872,f28713]) ).
fof(f28715,plain,
m1_subset_1(sK41,k1_zfmisc_1(k1_filter_0(sK39))),
inference(superposition,[],[f19873,f28713]) ).
fof(f28716,plain,
r1_filter_2(k1_filter_0(sK39),sK41,k6_domain_1(k1_filter_0(sK39),sK40)),
inference(superposition,[],[f19875,f28713]) ).
fof(f28719,plain,
! [X0] :
( r1_filter_2(k1_filter_0(sK39),k19_filter_2(sK39,X0),X0)
| ~ m2_filter_2(X0,sK39) ),
inference(superposition,[],[f28603,f28713]) ).
fof(f28753,plain,
sK41 = k7_filter_2(sK39,sK41),
inference(resolution,[],[f28672,f19873]) ).
fof(f28756,plain,
( k19_filter_2(sK39,sK41) = k3_filter_2(k1_lattice2(sK39),sK41)
| ~ spl869_43 ),
inference(superposition,[],[f28641,f28753]) ).
fof(f28757,plain,
( v3_struct_0(sK39)
| m1_filter_0(u1_struct_0(sK39),sK39)
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f19922,f19870]) ).
fof(f28758,plain,
( m1_filter_0(u1_struct_0(sK39),sK39)
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f28757,f19871]) ).
fof(f28759,plain,
m1_filter_0(u1_struct_0(sK39),sK39),
inference(forward_subsumption_resolution,[],[f28758,f19869]) ).
fof(f28760,plain,
m1_filter_0(k1_filter_0(sK39),sK39),
inference(forward_demodulation,[],[f28759,f28713]) ).
fof(f28786,plain,
l3_lattices(k1_lattice2(sK39)),
inference(resolution,[],[f20030,f19869]) ).
fof(f28788,plain,
( $false
| spl869_45 ),
inference(forward_subsumption_resolution,[],[f28786,f28693]) ).
fof(f28789,plain,
spl869_45,
inference(avatar_contradiction_clause,[],[f28788]) ).
fof(f28808,plain,
( v3_struct_0(sK39)
| v10_lattices(k1_lattice2(sK39))
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f20033,f19870]) ).
fof(f28810,plain,
( v10_lattices(k1_lattice2(sK39))
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f28808,f19871]) ).
fof(f28811,plain,
( ~ l3_lattices(sK39)
| spl869_46 ),
inference(forward_subsumption_resolution,[],[f28810,f28696]) ).
fof(f28812,plain,
( $false
| spl869_46 ),
inference(forward_subsumption_resolution,[],[f28811,f19869]) ).
fof(f28813,plain,
spl869_46,
inference(avatar_contradiction_clause,[],[f28812]) ).
fof(f28814,plain,
v10_lattices(k1_lattice2(sK39)),
inference(forward_subsumption_resolution,[],[f28810,f19869]) ).
fof(f28815,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK39))
| k3_filter_0(k1_lattice2(sK39),X0) = k3_filter_2(k1_lattice2(sK39),X0)
| ~ l3_lattices(k1_lattice2(sK39))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39)))) ),
inference(resolution,[],[f28814,f19703]) ).
fof(f28834,plain,
( v3_struct_0(sK39)
| ~ l3_lattices(sK39)
| ~ spl869_47 ),
inference(resolution,[],[f20043,f28699]) ).
fof(f28836,plain,
( ~ l3_lattices(sK39)
| ~ spl869_47 ),
inference(forward_subsumption_resolution,[],[f28834,f19871]) ).
fof(f28837,plain,
( $false
| ~ spl869_47 ),
inference(forward_subsumption_resolution,[],[f28836,f19869]) ).
fof(f28838,plain,
~ spl869_47,
inference(avatar_contradiction_clause,[],[f28837]) ).
fof(f28839,plain,
( ! [X0] :
( ~ m1_subset_1(k6_domain_1(k1_filter_0(sK39),X0),k1_zfmisc_1(k1_filter_0(sK39)))
| ~ m1_subset_1(X0,u1_struct_0(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k3_filter_0(k1_lattice2(sK39),k6_domain_1(u1_struct_0(sK39),X0))
| v1_xboole_0(k6_domain_1(u1_struct_0(sK39),X0)) )
| ~ spl869_48 ),
inference(forward_demodulation,[],[f28702,f28713]) ).
fof(f28855,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK39))
| k3_filter_0(k1_lattice2(sK39),X0) = k3_filter_2(k1_lattice2(sK39),X0)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39)))) ),
inference(forward_subsumption_resolution,[],[f28815,f28786]) ).
fof(f28856,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK39))
| ~ m1_subset_1(k6_domain_1(k1_filter_0(sK39),X0),k1_zfmisc_1(k1_filter_0(sK39)))
| k2_filter_0(k1_lattice2(sK39),X0) = k3_filter_0(k1_lattice2(sK39),k6_domain_1(u1_struct_0(sK39),X0))
| v1_xboole_0(k6_domain_1(u1_struct_0(sK39),X0)) )
| ~ spl869_48 ),
inference(forward_demodulation,[],[f28839,f28713]) ).
fof(f28875,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| v3_struct_0(k1_lattice2(sK39))
| k3_filter_0(k1_lattice2(sK39),X0) = k3_filter_2(k1_lattice2(sK39),X0)
| v1_xboole_0(X0) ),
inference(forward_demodulation,[],[f28855,f28688]) ).
fof(f28876,plain,
( ! [X0] :
( k2_filter_0(k1_lattice2(sK39),X0) = k3_filter_0(k1_lattice2(sK39),k6_domain_1(k1_filter_0(sK39),X0))
| ~ m1_subset_1(X0,k1_filter_0(sK39))
| ~ m1_subset_1(k6_domain_1(k1_filter_0(sK39),X0),k1_zfmisc_1(k1_filter_0(sK39)))
| v1_xboole_0(k6_domain_1(u1_struct_0(sK39),X0)) )
| ~ spl869_48 ),
inference(forward_demodulation,[],[f28856,f28713]) ).
fof(f28891,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| v3_struct_0(k1_lattice2(sK39))
| k3_filter_0(k1_lattice2(sK39),X0) = k3_filter_2(k1_lattice2(sK39),X0)
| v1_xboole_0(X0) ),
inference(forward_demodulation,[],[f28875,f28713]) ).
fof(f28892,plain,
( ! [X0] :
( ~ m1_subset_1(k6_domain_1(k1_filter_0(sK39),X0),k1_zfmisc_1(k1_filter_0(sK39)))
| k2_filter_0(k1_lattice2(sK39),X0) = k3_filter_0(k1_lattice2(sK39),k6_domain_1(k1_filter_0(sK39),X0))
| ~ m1_subset_1(X0,k1_filter_0(sK39))
| v1_xboole_0(k6_domain_1(k1_filter_0(sK39),X0)) )
| ~ spl869_48 ),
inference(forward_demodulation,[],[f28876,f28713]) ).
fof(f28938,definition,
( spl869_67
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK39),X0) = k3_filter_2(k1_lattice2(sK39),X0) ) ),
introduced(definition,[new_symbols(definition,[spl869_67])],[avatar_definition]) ).
fof(f28939,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK39),X0) = k3_filter_2(k1_lattice2(sK39),X0) )
| ~ spl869_67 ),
inference(avatar_component_clause,[],[f28938]) ).
fof(f28940,plain,
( spl869_47
| spl869_67 ),
inference(avatar_split_clause,[],[f28891,f28938,f28698]) ).
fof(f28942,definition,
( spl869_68
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl869_68])],[avatar_definition]) ).
fof(f28943,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| v1_xboole_0(X0) )
| ~ spl869_68 ),
inference(avatar_component_clause,[],[f28942]) ).
fof(f28969,plain,
( v1_xboole_0(sK41)
| k3_filter_2(k1_lattice2(sK39),sK41) = k3_filter_0(k1_lattice2(sK39),sK41)
| ~ spl869_67 ),
inference(resolution,[],[f28939,f28715]) ).
fof(f28971,plain,
( k3_filter_2(k1_lattice2(sK39),sK41) = k3_filter_0(k1_lattice2(sK39),sK41)
| ~ spl869_67 ),
inference(forward_subsumption_resolution,[],[f28969,f19874]) ).
fof(f28972,plain,
( k19_filter_2(sK39,sK41) = k3_filter_0(k1_lattice2(sK39),sK41)
| ~ spl869_43
| ~ spl869_67 ),
inference(forward_demodulation,[],[f28971,f28756]) ).
fof(f29020,plain,
( v1_xboole_0(sK41)
| ~ spl869_68 ),
inference(resolution,[],[f28943,f28715]) ).
fof(f29023,plain,
( $false
| ~ spl869_68 ),
inference(forward_subsumption_resolution,[],[f29020,f19874]) ).
fof(f29024,plain,
~ spl869_68,
inference(avatar_contradiction_clause,[],[f29023]) ).
fof(f29026,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k2_filter_2(k1_lattice2(sK39),X0)
| ~ l3_lattices(k1_lattice2(sK39))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK39))) ),
inference(resolution,[],[f19701,f28814]) ).
fof(f29027,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k2_filter_2(k1_lattice2(sK39),X0)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK39))) ),
inference(forward_subsumption_resolution,[],[f29026,f28786]) ).
fof(f29029,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| v3_struct_0(k1_lattice2(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k2_filter_2(k1_lattice2(sK39),X0) ),
inference(forward_demodulation,[],[f29027,f28688]) ).
fof(f29031,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK39))
| v3_struct_0(k1_lattice2(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k2_filter_2(k1_lattice2(sK39),X0) ),
inference(forward_demodulation,[],[f29029,f28713]) ).
fof(f29034,definition,
( spl869_79
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k2_filter_2(k1_lattice2(sK39),X0) ) ),
introduced(definition,[new_symbols(definition,[spl869_79])],[avatar_definition]) ).
fof(f29035,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK39))
| k2_filter_0(k1_lattice2(sK39),X0) = k2_filter_2(k1_lattice2(sK39),X0) )
| ~ spl869_79 ),
inference(avatar_component_clause,[],[f29034]) ).
fof(f29036,plain,
( spl869_47
| spl869_79 ),
inference(avatar_split_clause,[],[f29031,f29034,f28698]) ).
fof(f29039,plain,
! [X0] :
( v1_xboole_0(u1_struct_0(sK39))
| ~ r1_filter_2(u1_struct_0(sK39),sK41,k6_domain_1(u1_struct_0(sK39),X0))
| sK41 = k6_domain_1(u1_struct_0(sK39),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK39)) ),
inference(resolution,[],[f28660,f19873]) ).
fof(f29255,plain,
( k2_filter_0(k1_lattice2(sK39),sK40) = k2_filter_2(k1_lattice2(sK39),sK40)
| ~ spl869_79 ),
inference(resolution,[],[f29035,f28714]) ).
fof(f29310,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f19857,f19858]) ).
fof(f29311,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(duplicate_literal_removal,[],[f29310]) ).
fof(f29312,plain,
! [X0,X1] :
( k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f29311,f20550]) ).
fof(f29313,plain,
! [X0,X1] :
( ~ v10_lattices(X1)
| ~ m2_filter_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| k19_filter_2(X1,X0) = X0
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f29312,f19692]) ).
fof(f29314,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| v3_struct_0(sK39)
| k19_filter_2(sK39,X0) = X0
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f29313,f19870]) ).
fof(f29317,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| k19_filter_2(sK39,X0) = X0
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f29314,f19871]) ).
fof(f29319,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| k19_filter_2(sK39,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f29317,f19869]) ).
fof(f29321,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| ~ m2_filter_2(X0,sK39)
| k19_filter_2(sK39,X0) = X0 ),
inference(forward_demodulation,[],[f29319,f28713]) ).
fof(f29540,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| v1_xboole_0(X0) )
| ~ spl869_44 ),
inference(forward_demodulation,[],[f28637,f28688]) ).
fof(f29562,definition,
( spl869_128
<=> v1_xboole_0(k1_filter_0(sK39)) ),
introduced(definition,[new_symbols(definition,[spl869_128])],[avatar_definition]) ).
fof(f29563,plain,
( v1_xboole_0(k1_filter_0(sK39))
| ~ spl869_128 ),
inference(avatar_component_clause,[],[f29562]) ).
fof(f29591,definition,
( spl869_135
<=> ! [X0] :
( ~ r1_filter_2(k1_filter_0(sK39),sK41,k6_domain_1(k1_filter_0(sK39),X0))
| ~ m1_subset_1(X0,k1_filter_0(sK39))
| sK41 = k6_domain_1(k1_filter_0(sK39),X0) ) ),
introduced(definition,[new_symbols(definition,[spl869_135])],[avatar_definition]) ).
fof(f29592,plain,
( ! [X0] :
( ~ r1_filter_2(k1_filter_0(sK39),sK41,k6_domain_1(k1_filter_0(sK39),X0))
| ~ m1_subset_1(X0,k1_filter_0(sK39))
| sK41 = k6_domain_1(k1_filter_0(sK39),X0) )
| ~ spl869_135 ),
inference(avatar_component_clause,[],[f29591]) ).
fof(f29594,plain,
! [X0] :
( v1_xboole_0(k1_filter_0(sK39))
| ~ r1_filter_2(u1_struct_0(sK39),sK41,k6_domain_1(u1_struct_0(sK39),X0))
| sK41 = k6_domain_1(u1_struct_0(sK39),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK39)) ),
inference(forward_demodulation,[],[f29039,f28713]) ).
fof(f29702,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| v1_xboole_0(X0) )
| ~ spl869_44 ),
inference(forward_demodulation,[],[f29540,f28713]) ).
fof(f29708,plain,
! [X0] :
( ~ r1_filter_2(k1_filter_0(sK39),sK41,k6_domain_1(k1_filter_0(sK39),X0))
| v1_xboole_0(k1_filter_0(sK39))
| sK41 = k6_domain_1(u1_struct_0(sK39),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK39)) ),
inference(forward_demodulation,[],[f29594,f28713]) ).
fof(f29721,plain,
( spl869_68
| ~ spl869_44 ),
inference(avatar_split_clause,[],[f29702,f28636,f28942]) ).
fof(f29727,plain,
! [X0] :
( sK41 = k6_domain_1(k1_filter_0(sK39),X0)
| ~ r1_filter_2(k1_filter_0(sK39),sK41,k6_domain_1(k1_filter_0(sK39),X0))
| v1_xboole_0(k1_filter_0(sK39))
| ~ m1_subset_1(X0,u1_struct_0(sK39)) ),
inference(forward_demodulation,[],[f29708,f28713]) ).
fof(f29737,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK39))
| sK41 = k6_domain_1(k1_filter_0(sK39),X0)
| ~ r1_filter_2(k1_filter_0(sK39),sK41,k6_domain_1(k1_filter_0(sK39),X0))
| v1_xboole_0(k1_filter_0(sK39)) ),
inference(forward_demodulation,[],[f29727,f28713]) ).
fof(f29746,plain,
( spl869_128
| spl869_135 ),
inference(avatar_split_clause,[],[f29737,f29591,f29562]) ).
fof(f29773,plain,
( $false
| ~ spl869_128 ),
inference(unit_resulting_resolution,[],[f19921,f19869,f19870,f19871,f28760,f29563]) ).
fof(f29774,plain,
~ spl869_128,
inference(avatar_contradiction_clause,[],[f29773]) ).
fof(f29858,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(resolution,[],[f19802,f19689]) ).
fof(f29859,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(forward_subsumption_resolution,[],[f29858,f20043]) ).
fof(f29860,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(forward_subsumption_resolution,[],[f29859,f20033]) ).
fof(f29861,plain,
! [X0,X1] :
( ~ v10_lattices(X1)
| v3_struct_0(X1)
| ~ m2_filter_2(X0,X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1)) ),
inference(forward_subsumption_resolution,[],[f29860,f20030]) ).
fof(f29862,plain,
! [X0] :
( v3_struct_0(sK39)
| ~ m2_filter_2(X0,sK39)
| ~ l3_lattices(sK39)
| m1_filter_0(X0,k1_lattice2(sK39)) ),
inference(resolution,[],[f29861,f19870]) ).
fof(f29865,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| ~ l3_lattices(sK39)
| m1_filter_0(X0,k1_lattice2(sK39)) ),
inference(forward_subsumption_resolution,[],[f29862,f19871]) ).
fof(f29870,plain,
! [X0] :
( m1_filter_0(X0,k1_lattice2(sK39))
| ~ m2_filter_2(X0,sK39) ),
inference(forward_subsumption_resolution,[],[f29865,f19869]) ).
fof(f29873,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39))))
| v3_struct_0(k1_lattice2(sK39))
| ~ v10_lattices(k1_lattice2(sK39))
| ~ l3_lattices(k1_lattice2(sK39)) ),
inference(resolution,[],[f29870,f19920]) ).
fof(f29875,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39))))
| v3_struct_0(k1_lattice2(sK39))
| ~ l3_lattices(k1_lattice2(sK39)) ),
inference(forward_subsumption_resolution,[],[f29873,f28814]) ).
fof(f29878,plain,
! [X0] :
( ~ m2_filter_2(X0,sK39)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK39))))
| v3_struct_0(k1_lattice2(sK39)) ),
inference(forward_subsumption_resolution,[],[f29875,f28786]) ).
fof(f29880,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK39)))
| ~ m2_filter_2(X0,sK39)
| v3_struct_0(k1_lattice2(sK39)) ),
inference(forward_demodulation,[],[f29878,f28688]) ).
fof(f29882,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| ~ m2_filter_2(X0,sK39)
| v3_struct_0(k1_lattice2(sK39)) ),
inference(forward_demodulation,[],[f29880,f28713]) ).
fof(f29885,definition,
( spl869_176
<=> ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39)))
| ~ m2_filter_2(X0,sK39) ) ),
introduced(definition,[new_symbols(definition,[spl869_176])],[avatar_definition]) ).
fof(f29886,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK39)
| m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK39))) )
| ~ spl869_176 ),
inference(avatar_component_clause,[],[f29885]) ).
fof(f29887,plain,
( spl869_47
| spl869_176 ),
inference(avatar_split_clause,[],[f29882,f29885,f28698]) ).
fof(f29894,plain,
( m1_subset_1(a_2_0_filter_2(sK39,sK40),k1_zfmisc_1(k1_filter_0(sK39)))
| ~ spl869_176 ),
inference(resolution,[],[f29886,f28651]) ).
fof(f30008,plain,
( ~ m2_filter_2(a_2_0_filter_2(sK39,sK40),sK39)
| a_2_0_filter_2(sK39,sK40) = k19_filter_2(sK39,a_2_0_filter_2(sK39,sK40))
| ~ spl869_176 ),
inference(resolution,[],[f29894,f29321]) ).
fof(f30049,plain,
( a_2_0_filter_2(sK39,sK40) = k19_filter_2(sK39,a_2_0_filter_2(sK39,sK40))
| ~ spl869_176 ),
inference(forward_subsumption_resolution,[],[f30008,f28651]) ).
fof(f30078,plain,
( r1_filter_2(k1_filter_0(sK39),a_2_0_filter_2(sK39,sK40),a_2_0_filter_2(sK39,sK40))
| ~ m2_filter_2(a_2_0_filter_2(sK39,sK40),sK39)
| ~ spl869_176 ),
inference(superposition,[],[f28719,f30049]) ).
fof(f30085,plain,
( r1_filter_2(k1_filter_0(sK39),a_2_0_filter_2(sK39,sK40),a_2_0_filter_2(sK39,sK40))
| ~ spl869_176 ),
inference(forward_subsumption_resolution,[],[f30078,f28651]) ).
fof(f30315,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| v3_struct_0(sK39)
| k5_filter_2(sK39,X0) = X0
| ~ l3_lattices(sK39) ),
inference(resolution,[],[f19790,f19870]) ).
fof(f30318,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| k5_filter_2(sK39,X0) = X0
| ~ l3_lattices(sK39) ),
inference(forward_subsumption_resolution,[],[f30315,f19871]) ).
fof(f30320,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK39))
| k5_filter_2(sK39,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f30318,f19869]) ).
fof(f30322,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK39))
| k5_filter_2(sK39,X0) = X0 ),
inference(forward_demodulation,[],[f30320,f28713]) ).
fof(f30327,plain,
sK40 = k5_filter_2(sK39,sK40),
inference(resolution,[],[f30322,f28714]) ).
fof(f30328,plain,
k18_filter_2(sK39,sK40) = k2_filter_2(k1_lattice2(sK39),sK40),
inference(superposition,[],[f28628,f30327]) ).
fof(f30329,plain,
a_2_0_filter_2(sK39,sK40) = k2_filter_2(k1_lattice2(sK39),sK40),
inference(forward_demodulation,[],[f30328,f28642]) ).
fof(f30331,plain,
( a_2_0_filter_2(sK39,sK40) = k2_filter_0(k1_lattice2(sK39),sK40)
| ~ spl869_79 ),
inference(superposition,[],[f29255,f30329]) ).
fof(f36733,plain,
( ~ m1_subset_1(sK40,k1_filter_0(sK39))
| sK41 = k6_domain_1(k1_filter_0(sK39),sK40)
| ~ spl869_135 ),
inference(resolution,[],[f29592,f28716]) ).
fof(f36736,plain,
( sK41 = k6_domain_1(k1_filter_0(sK39),sK40)
| ~ spl869_135 ),
inference(forward_subsumption_resolution,[],[f36733,f28714]) ).
fof(f40511,definition,
( spl869_1067
<=> k19_filter_2(sK39,sK41) = a_2_0_filter_2(sK39,sK40) ),
introduced(definition,[new_symbols(definition,[spl869_1067])],[avatar_definition]) ).
fof(f40512,plain,
( k19_filter_2(sK39,sK41) = a_2_0_filter_2(sK39,sK40)
| ~ spl869_1067 ),
inference(avatar_component_clause,[],[f40511]) ).
fof(f42767,plain,
( ~ m1_subset_1(sK41,k1_zfmisc_1(k1_filter_0(sK39)))
| k3_filter_0(k1_lattice2(sK39),sK41) = k2_filter_0(k1_lattice2(sK39),sK40)
| ~ m1_subset_1(sK40,k1_filter_0(sK39))
| v1_xboole_0(sK41)
| ~ spl869_48
| ~ spl869_135 ),
inference(superposition,[],[f28892,f36736]) ).
fof(f42771,plain,
( k3_filter_0(k1_lattice2(sK39),sK41) = k2_filter_0(k1_lattice2(sK39),sK40)
| ~ m1_subset_1(sK40,k1_filter_0(sK39))
| v1_xboole_0(sK41)
| ~ spl869_48
| ~ spl869_135 ),
inference(forward_subsumption_resolution,[],[f42767,f28715]) ).
fof(f42773,plain,
( k3_filter_0(k1_lattice2(sK39),sK41) = k2_filter_0(k1_lattice2(sK39),sK40)
| v1_xboole_0(sK41)
| ~ spl869_48
| ~ spl869_135 ),
inference(forward_subsumption_resolution,[],[f42771,f28714]) ).
fof(f42775,plain,
( k3_filter_0(k1_lattice2(sK39),sK41) = k2_filter_0(k1_lattice2(sK39),sK40)
| ~ spl869_48
| ~ spl869_135 ),
inference(forward_subsumption_resolution,[],[f42773,f19874]) ).
fof(f42777,plain,
( a_2_0_filter_2(sK39,sK40) = k3_filter_0(k1_lattice2(sK39),sK41)
| ~ spl869_48
| ~ spl869_79
| ~ spl869_135 ),
inference(forward_demodulation,[],[f42775,f30331]) ).
fof(f42780,plain,
( k19_filter_2(sK39,sK41) = a_2_0_filter_2(sK39,sK40)
| ~ spl869_43
| ~ spl869_48
| ~ spl869_67
| ~ spl869_79
| ~ spl869_135 ),
inference(superposition,[],[f28972,f42777]) ).
fof(f42781,plain,
( spl869_1067
| ~ spl869_43
| ~ spl869_48
| ~ spl869_67
| ~ spl869_79
| ~ spl869_135 ),
inference(avatar_split_clause,[],[f42780,f29591,f29034,f28938,f28701,f28633,f40511]) ).
fof(f42782,plain,
( ~ r1_filter_2(u1_struct_0(sK39),a_2_0_filter_2(sK39,sK40),k18_filter_2(sK39,sK40))
| ~ spl869_1067 ),
inference(superposition,[],[f19876,f40512]) ).
fof(f42887,plain,
( ~ r1_filter_2(u1_struct_0(sK39),a_2_0_filter_2(sK39,sK40),a_2_0_filter_2(sK39,sK40))
| ~ spl869_1067 ),
inference(forward_demodulation,[],[f42782,f28642]) ).
fof(f42896,plain,
( ~ r1_filter_2(k1_filter_0(sK39),a_2_0_filter_2(sK39,sK40),a_2_0_filter_2(sK39,sK40))
| ~ spl869_1067 ),
inference(forward_demodulation,[],[f42887,f28713]) ).
fof(f42898,plain,
( $false
| ~ spl869_176
| ~ spl869_1067 ),
inference(forward_subsumption_resolution,[],[f42896,f30085]) ).
fof(f42899,plain,
( ~ spl869_176
| ~ spl869_1067 ),
inference(avatar_contradiction_clause,[],[f42898]) ).
cnf(s36,plain,
( spl869_43
| spl869_44 ),
inference(sat_conversion,[],[f28638]) ).
cnf(s37,plain,
( ~ spl869_45
| ~ spl869_46
| spl869_47
| spl869_48 ),
inference(sat_conversion,[],[f28703]) ).
cnf(s42,plain,
spl869_45,
inference(sat_conversion,[],[f28789]) ).
cnf(s45,plain,
spl869_46,
inference(sat_conversion,[],[f28813]) ).
cnf(s47,plain,
~ spl869_47,
inference(sat_conversion,[],[f28838]) ).
cnf(s59,plain,
( spl869_47
| spl869_67 ),
inference(sat_conversion,[],[f28940]) ).
cnf(s71,plain,
~ spl869_68,
inference(sat_conversion,[],[f29024]) ).
cnf(s72,plain,
( spl869_47
| spl869_79 ),
inference(sat_conversion,[],[f29036]) ).
cnf(s150,plain,
( ~ spl869_44
| spl869_68 ),
inference(sat_conversion,[],[f29721]) ).
cnf(s159,plain,
( spl869_128
| spl869_135 ),
inference(sat_conversion,[],[f29746]) ).
cnf(s162,plain,
~ spl869_128,
inference(sat_conversion,[],[f29774]) ).
cnf(s174,plain,
( spl869_47
| spl869_176 ),
inference(sat_conversion,[],[f29887]) ).
cnf(s1204,plain,
( ~ spl869_43
| ~ spl869_48
| ~ spl869_67
| ~ spl869_79
| ~ spl869_135
| spl869_1067 ),
inference(sat_conversion,[],[f42781]) ).
cnf(s1212,plain,
( ~ spl869_176
| ~ spl869_1067 ),
inference(sat_conversion,[],[f42899]) ).
cnf(s1295,plain,
spl869_135,
inference(rat,[],[s159,s162]) ).
cnf(s1375,plain,
~ spl869_44,
inference(rat,[],[s150,s71]) ).
cnf(s1454,plain,
spl869_176,
inference(rat,[],[s174,s47]) ).
cnf(s1464,plain,
spl869_79,
inference(rat,[],[s72,s47]) ).
cnf(s1467,plain,
spl869_67,
inference(rat,[],[s59,s47]) ).
cnf(s1484,plain,
~ spl869_1067,
inference(rat,[],[s1212,s1454]) ).
cnf(s1686,plain,
spl869_48,
inference(rat,[],[s37,s47,s45,s42]) ).
cnf(s1687,plain,
~ spl869_43,
inference(rat,[],[s1204,s1484,s1295,s1464,s1467,s1686]) ).
cnf(s1688,plain,
$false,
inference(rat,[],[s36,s1375,s1687]) ).
fof(f42900,plain,
$false,
inference(avatar_sat_refutation,[],[s1688]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT312+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.12/0.40 % Computer : n009.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 14:31:02 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.46 Running first-order theorem proving
% 0.12/0.46 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
% 24.25/5.19 % (2099202)Detected formulas, will run a generic FOF schedule.
% 24.25/5.19 % (2099228)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=621567596:i=141193_2990 on theBenchmark for (2990ds/141193Mi)
% 24.25/5.19 % (2099231)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2124992005:i=109:sd=1:ins=1:gsp=on:ss=axioms_2990 on theBenchmark for (2990ds/109Mi)
% 24.25/5.19 % (2099232)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2380809604:i=119:av=off:ss=axioms_2990 on theBenchmark for (2990ds/119Mi)
% 24.25/5.19 % (2099230)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=213924311:i=141695:sd=1:nm=32:gsp=on:ss=included_2990 on theBenchmark for (2990ds/141695Mi)
% 24.25/5.19 % (2099229)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=2550157225:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2990 on theBenchmark for (2990ds/134677Mi)
% 24.25/5.19 % (2099233)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=653671556:s2a=on:i=139:gtg=position_2990 on theBenchmark for (2990ds/139Mi)
% 24.25/5.19 % (2099234)dis-21_1_sil=8000:lcm=predicate:random_seed=3340291897:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2990 on theBenchmark for (2990ds/129Mi)
% 24.25/5.19 % (2099231)Instruction limit reached!
% 24.25/5.19 % (2099231)------------------------------
% 24.25/5.19 % (2099231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.25/5.19 % (2099231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.25/5.19 % (2099231)CaDiCaL version: 2.1.3
% 24.25/5.19 % (2099231)Termination reason: Instruction limit
% 24.25/5.19 % (2099231)Termination phase: Saturation
% 24.25/5.19 % (2099231)Time elapsed: 0.121 s
% 24.25/5.19 % (2099231)Peak memory usage: 107 MB
% 24.25/5.19 % (2099231)Instructions burned: 109 (million)
% 24.25/5.19 % (2099233)Instruction limit reached!
% 24.25/5.19 % (2099233)------------------------------
% 24.25/5.19 % (2099233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.25/5.19 % (2099233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.25/5.19 % (2099233)CaDiCaL version: 2.1.3
% 24.25/5.19 % (2099233)Termination reason: Instruction limit
% 24.25/5.19 % (2099233)Termination phase: Property scanning
% 24.25/5.19 % (2099233)Time elapsed: 0.114 s
% 24.25/5.19 % (2099233)Peak memory usage: 102 MB
% 24.25/5.19 % (2099233)Instructions burned: 139 (million)
% 24.25/5.19 % (2099232)Instruction limit reached!
% 24.25/5.19 % (2099232)------------------------------
% 24.25/5.19 % (2099232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.25/5.19 % (2099232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.25/5.19 % (2099232)CaDiCaL version: 2.1.3
% 24.25/5.19 % (2099232)Termination reason: Instruction limit
% 24.25/5.19 % (2099232)Termination phase: Function definition elimination
% 24.25/5.19 % (2099232)Time elapsed: 0.137 s
% 24.25/5.19 % (2099232)Peak memory usage: 105 MB
% 24.25/5.19 % (2099232)Instructions burned: 120 (million)
% 24.25/5.19 % (2099234)Instruction limit reached!
% 24.25/5.19 % (2099234)------------------------------
% 24.25/5.19 % (2099234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.25/5.19 % (2099234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.25/5.19 % (2099234)CaDiCaL version: 2.1.3
% 24.25/5.19 % (2099234)Termination reason: Instruction limit
% 24.25/5.19 % (2099234)Termination phase: Preprocessing 1
% 24.25/5.19 % (2099234)Time elapsed: 0.150 s
% 24.25/5.19 % (2099234)Peak memory usage: 104 MB
% 24.25/5.19 % (2099234)Instructions burned: 129 (million)
% 24.25/5.19 % (2099244)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2457036587:i=325:sd=1:ss=axioms:sgt=32_2987 on theBenchmark for (2987ds/325Mi)
% 24.25/5.19 % (2099242)lrs+10_1_sil=8000:sp=occurrence:random_seed=3617899578:i=285:sd=3:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/285Mi)
% 24.25/5.19 % (2099243)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2583556508:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/157Mi)
% 24.25/5.19 % (2099245)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=3504182351:s2a=on:i=248:s2at=1.23:gtg=position_2987 on theBenchmark for (2987ds/248Mi)
% 31.57/6.26 % (2099243)Instruction limit reached!
% 31.57/6.26 % (2099243)------------------------------
% 31.57/6.26 % (2099243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/6.26 % (2099243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/6.26 % (2099243)CaDiCaL version: 2.1.3
% 31.57/6.26 % (2099243)Termination reason: Instruction limit
% 31.57/6.26 % (2099243)Termination phase: Property scanning
% 31.57/6.26 % (2099243)Time elapsed: 0.132 s
% 31.57/6.26 % (2099243)Peak memory usage: 102 MB
% 31.57/6.26 % (2099243)Instructions burned: 158 (million)
% 31.57/6.26 % (2099245)Instruction limit reached!
% 31.57/6.26 % (2099245)------------------------------
% 31.57/6.26 % (2099245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/6.26 % (2099244)Instruction limit reached!
% 31.57/6.26 % (2099244)------------------------------
% 31.57/6.26 % (2099244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/6.26 % (2099244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/6.26 % (2099245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/6.26 % (2099244)CaDiCaL version: 2.1.3
% 31.57/6.26 % (2099245)CaDiCaL version: 2.1.3
% 31.57/6.26 % (2099244)Termination reason: Instruction limit
% 31.57/6.26 % (2099244)Termination phase: Saturation
% 31.57/6.26 % (2099244)Time elapsed: 0.335 s
% 31.57/6.26 % (2099245)Termination reason: Instruction limit
% 31.57/6.26 % (2099245)Termination phase: SInE selection
% 31.57/6.26 % (2099244)Peak memory usage: 108 MB
% 31.57/6.26 % (2099245)Time elapsed: 0.227 s
% 31.57/6.26 % (2099244)Instructions burned: 326 (million)
% 31.57/6.26 % (2099245)Peak memory usage: 103 MB
% 31.57/6.26 % (2099245)Instructions burned: 249 (million)
% 31.57/6.26 % (2099242)Instruction limit reached!
% 31.57/6.26 % (2099242)------------------------------
% 31.57/6.26 % (2099242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/6.26 % (2099242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/6.26 % (2099242)CaDiCaL version: 2.1.3
% 31.57/6.26 % (2099242)Termination reason: Instruction limit
% 31.57/6.26 % (2099242)Termination phase: Saturation
% 31.57/6.26 % (2099242)Time elapsed: 0.328 s
% 31.57/6.26 % (2099242)Peak memory usage: 110 MB
% 31.57/6.26 % (2099242)Instructions burned: 285 (million)
% 31.57/6.26 % (2099250)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3402894220:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 31.57/6.26 % (2099251)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3181753006:i=2350_2982 on theBenchmark for (2982ds/2350Mi)
% 31.57/6.26 % (2099253)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1911065861:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 31.57/6.26 % (2099252)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2270807354:cts=off:i=113:fsr=off:ss=included:sgt=4_2982 on theBenchmark for (2982ds/113Mi)
% 31.57/6.26 % (2099250)Instruction limit reached!
% 31.57/6.26 % (2099250)------------------------------
% 31.57/6.26 % (2099250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/6.26 % (2099250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/6.26 % (2099250)CaDiCaL version: 2.1.3
% 31.57/6.26 % (2099250)Termination reason: Instruction limit
% 31.57/6.26 % (2099250)Termination phase: Saturation
% 31.57/6.26 % (2099250)Time elapsed: 0.299 s
% 31.57/6.26 % (2099250)Peak memory usage: 110 MB
% 31.57/6.26 % (2099250)Instructions burned: 295 (million)
% 31.57/6.26 % (2099252)Instruction limit reached!
% 31.57/6.26 % (2099252)------------------------------
% 31.57/6.26 % (2099252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/6.26 % (2099252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/6.26 % (2099252)CaDiCaL version: 2.1.3
% 31.57/6.26 % (2099252)Termination reason: Instruction limit
% 31.57/6.26 % (2099252)Termination phase: Preprocessing 3
% 31.57/6.26 % (2099252)Time elapsed: 0.145 s
% 31.57/6.26 % (2099252)Peak memory usage: 105 MB
% 31.57/6.26 % (2099252)Instructions burned: 113 (million)
% 31.57/6.26 % (2099253)Instruction limit reached!
% 31.57/6.26 % (2099253)------------------------------
% 31.57/6.26 % (2099253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/6.26 % (2099253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/6.26 % (2099253)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099253)Termination reason: Instruction limit
% 42.71/9.52 % (2099253)Termination phase: Preprocessing 2
% 42.71/9.52 % (2099253)Time elapsed: 0.156 s
% 42.71/9.52 % (2099253)Peak memory usage: 106 MB
% 42.71/9.52 % (2099253)Instructions burned: 127 (million)
% 42.71/9.52 % (2099258)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1324105394:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2978 on theBenchmark for (2978ds/114Mi)
% 42.71/9.52 % (2099259)lrs+10_1_sil=8000:sp=occurrence:random_seed=524896539:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2978 on theBenchmark for (2978ds/907Mi)
% 42.71/9.52 % (2099260)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1760498721:i=437:sd=1:aac=none:ss=included_2978 on theBenchmark for (2978ds/437Mi)
% 42.71/9.52 % (2099258)Instruction limit reached!
% 42.71/9.52 % (2099258)------------------------------
% 42.71/9.52 % (2099258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099258)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099258)Termination reason: Instruction limit
% 42.71/9.52 % (2099258)Termination phase: Property scanning
% 42.71/9.52 % (2099258)Time elapsed: 0.094 s
% 42.71/9.52 % (2099258)Peak memory usage: 102 MB
% 42.71/9.52 % (2099258)Instructions burned: 115 (million)
% 42.71/9.52 % (2099266)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2694008727:i=5202:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/5202Mi)
% 42.71/9.52 % (2099260)Instruction limit reached!
% 42.71/9.52 % (2099260)------------------------------
% 42.71/9.52 % (2099260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099260)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099260)Termination reason: Instruction limit
% 42.71/9.52 % (2099260)Termination phase: Saturation
% 42.71/9.52 % (2099260)Time elapsed: 0.420 s
% 42.71/9.52 % (2099260)Peak memory usage: 109 MB
% 42.71/9.52 % (2099260)Instructions burned: 438 (million)
% 42.71/9.52 % (2099268)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=73068452:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2972 on theBenchmark for (2972ds/134Mi)
% 42.71/9.52 % (2099268)Instruction limit reached!
% 42.71/9.52 % (2099268)------------------------------
% 42.71/9.52 % (2099268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099268)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099268)Termination reason: Instruction limit
% 42.71/9.52 % (2099268)Termination phase: Property scanning
% 42.71/9.52 % (2099268)Time elapsed: 0.153 s
% 42.71/9.52 % (2099268)Peak memory usage: 106 MB
% 42.71/9.52 % (2099268)Instructions burned: 135 (million)
% 42.71/9.52 % (2099259)Instruction limit reached!
% 42.71/9.52 % (2099259)------------------------------
% 42.71/9.52 % (2099259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099259)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099259)Termination reason: Instruction limit
% 42.71/9.52 % (2099259)Termination phase: Saturation
% 42.71/9.52 % (2099259)Time elapsed: 0.955 s
% 42.71/9.52 % (2099259)Peak memory usage: 121 MB
% 42.71/9.52 % (2099259)Instructions burned: 907 (million)
% 42.71/9.52 % (2099270)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3245014101:st=8:i=592:sd=3:ep=RST:ss=axioms_2968 on theBenchmark for (2968ds/592Mi)
% 42.71/9.52 % (2099271)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1689306085:st=3:i=13193:sd=3:ss=axioms_2966 on theBenchmark for (2966ds/13193Mi)
% 42.71/9.52 % (2099270)Instruction limit reached!
% 42.71/9.52 % (2099270)------------------------------
% 42.71/9.52 % (2099270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099270)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099270)Termination reason: Instruction limit
% 42.71/9.52 % (2099270)Termination phase: Property scanning
% 42.71/9.52 % (2099270)Time elapsed: 0.600 s
% 42.71/9.52 % (2099270)Peak memory usage: 125 MB
% 42.71/9.52 % (2099270)Instructions burned: 593 (million)
% 42.71/9.52 % (2099274)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=205825570:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/125Mi)
% 42.71/9.52 % (2099274)Instruction limit reached!
% 42.71/9.52 % (2099274)------------------------------
% 42.71/9.52 % (2099274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099274)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099274)Termination reason: Instruction limit
% 42.71/9.52 % (2099274)Termination phase: Property scanning
% 42.71/9.52 % (2099274)Time elapsed: 0.105 s
% 42.71/9.52 % (2099274)Peak memory usage: 102 MB
% 42.71/9.52 % (2099274)Instructions burned: 125 (million)
% 42.71/9.52 % (2099251)Instruction limit reached!
% 42.71/9.52 % (2099251)------------------------------
% 42.71/9.52 % (2099251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099251)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099251)Termination reason: Instruction limit
% 42.71/9.52 % (2099251)Termination phase: Saturation
% 42.71/9.52 % (2099251)Time elapsed: 2.432 s
% 42.71/9.52 % (2099251)Peak memory usage: 238 MB
% 42.71/9.52 % (2099251)Instructions burned: 2351 (million)
% 42.71/9.52 % (2099276)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2954975566:i=134:gtgl=5:slsql=off:gtg=exists_sym_2957 on theBenchmark for (2957ds/134Mi)
% 42.71/9.52 % (2099276)Instruction limit reached!
% 42.71/9.52 % (2099276)------------------------------
% 42.71/9.52 % (2099276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099276)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099276)Termination reason: Instruction limit
% 42.71/9.52 % (2099276)Termination phase: Property scanning
% 42.71/9.52 % (2099276)Time elapsed: 0.113 s
% 42.71/9.52 % (2099276)Peak memory usage: 102 MB
% 42.71/9.52 % (2099276)Instructions burned: 135 (million)
% 42.71/9.52 % (2099278)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3057264645:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/141Mi)
% 42.71/9.52 % (2099281)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4081095636:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2953 on theBenchmark for (2953ds/431Mi)
% 42.71/9.52 % (2099278)Instruction limit reached!
% 42.71/9.52 % (2099278)------------------------------
% 42.71/9.52 % (2099278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099278)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099278)Termination reason: Instruction limit
% 42.71/9.52 % (2099278)Termination phase: Saturation
% 42.71/9.52 % (2099278)Time elapsed: 0.156 s
% 42.71/9.52 % (2099278)Peak memory usage: 108 MB
% 42.71/9.52 % (2099278)Instructions burned: 141 (million)
% 42.71/9.52 % (2099284)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2956148387:i=6060:aac=none:ins=25_2951 on theBenchmark for (2951ds/6060Mi)
% 42.71/9.52 % (2099281)Instruction limit reached!
% 42.71/9.52 % (2099281)------------------------------
% 42.71/9.52 % (2099281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099281)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099281)Termination reason: Instruction limit
% 42.71/9.52 % (2099281)Termination phase: Saturation
% 42.71/9.52 % (2099281)Time elapsed: 0.239 s
% 42.71/9.52 % (2099281)Peak memory usage: 111 MB
% 42.71/9.52 % (2099281)Instructions burned: 434 (million)
% 42.71/9.52 % (2099288)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3972700727:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2949 on theBenchmark for (2949ds/150Mi)
% 42.71/9.52 % (2099288)Instruction limit reached!
% 42.71/9.52 % (2099288)------------------------------
% 42.71/9.52 % (2099288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.71/9.52 % (2099288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.71/9.52 % (2099288)CaDiCaL version: 2.1.3
% 42.71/9.52 % (2099288)Termination reason: Instruction limit
% 42.71/9.52 % (2099288)Termination phase: Preprocessing 1
% 42.71/9.52 % (2099288)Time elapsed: 0.097 s
% 42.71/9.52 % (2099288)Peak memory usage: 103 MB
% 42.71/9.52 % (2099288)Instructions burned: 151 (million)
% 42.71/9.52 % (2099290)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1176351757:i=14155:bd=all_2947 on theBenchmark for (2947ds/14155Mi)
% 42.71/9.52 % (2099229)First to succeed.
% 42.71/9.52 % (2099229)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2099202"
% 42.71/9.52 % (2099229)Refutation found. Thanks to Tanya!
% 42.71/9.52 % SZS status Theorem for theBenchmark
% 42.71/9.52 % SZS output start Proof for theBenchmark
% See solution above
% 53.89/9.72 % (2099229)------------------------------
% 53.89/9.72 % (2099229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.89/9.72 % (2099229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.89/9.72 % (2099229)CaDiCaL version: 2.1.3
% 53.89/9.72 % (2099229)Termination reason: Refutation
% 53.89/9.72 % (2099229)Time elapsed: 6.340 s
% 53.89/9.72 % (2099229)Peak memory usage: 229 MB
% 53.89/9.72 % (2099229)Instructions burned: 6034 (million)
% 53.89/9.72 % (2099229)------------------------------
% 53.89/9.72 % (2099229)------------------------------
% 53.89/9.72 % (2099202)Success in time 8.511 s
% 53.89/9.72 % Vampire exiting
%------------------------------------------------------------------------------