%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT318+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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:52 AM UTC 2026
% Result : Theorem 40.83s 6.45s
% Output : Refutation 41.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 56
% Syntax : Number of formulae : 450 ( 74 unt; 23 def)
% Number of atoms : 1866 ( 217 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 2363 ( 947 ~;1155 |; 187 &)
% ( 26 <=>; 48 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 18 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 8 con; 0-3 aty)
% Number of variables : 450 ( 0 sgn 439 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
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(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f73,axiom,
! [X0,X1,X2] : k2_xboole_0(k2_xboole_0(X0,X1),X2) = k2_xboole_0(X0,k2_xboole_0(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_xboole_1) ).
fof(f81,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
=> k2_xboole_0(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f163,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k3_xboole_0(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t94_xboole_1) ).
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f356,axiom,
! [X0] : k3_tarski(k1_tarski(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_zfmisc_1) ).
fof(f418,axiom,
! [X0,X1] : k3_tarski(k2_tarski(X0,X1)) = k2_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t93_zfmisc_1) ).
fof(f567,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_subset_1) ).
fof(f568,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k4_subset_1) ).
fof(f570,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
fof(f2495,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ! [X2] :
( m1_filter_0(X2,X0)
=> k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k5_filter_0(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t50_filter_0) ).
fof(f2540,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/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f2564,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
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(f2597,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/sandbox2/benchmark/theBenchmark.p',t18_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(f2873,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/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f2874,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(f2884,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/sandbox2/benchmark/theBenchmark.p',redefinition_k3_filter_2) ).
fof(f2903,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f2904,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> k15_filter_2(X0,X1) = k7_filter_2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f2910,axiom,
! [X0,X1,X2] :
( ( ~ 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)))
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> m1_subset_1(k20_filter_2(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k20_filter_2) ).
fof(f2943,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(f2965,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(f2967,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(f2977,axiom,
! [X0,X1,X2] :
( ( ~ 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)))
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ~ v1_xboole_0(k20_filter_2(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_filter_2) ).
fof(f2979,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(X0))) )
=> ! [X3] :
( ( ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ! [X4] :
( ( ~ v1_xboole_0(X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t45_filter_2) ).
fof(f2983,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(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),k19_filter_2(X0,X1),X2)))
& r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,k19_filter_2(X0,X2)))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t49_filter_2) ).
fof(f2986,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k20_filter_2(X0,X1,X2))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t52_filter_2) ).
fof(f2987,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k20_filter_2(X0,X1,X2))) ) ) ),
inference(negated_conjecture,[status(cth)],[f2986]) ).
fof(f3079,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f3102,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f3112,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = X1
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f81]) ).
fof(f3387,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f567]) ).
fof(f3388,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f3387]) ).
fof(f3389,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f568]) ).
fof(f3390,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f3389]) ).
fof(f3393,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f570]) ).
fof(f3394,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f3393]) ).
fof(f5545,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k5_filter_0(X0,X1,X2))
| ~ m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2495]) ).
fof(f5546,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k5_filter_0(X0,X1,X2))
| ~ m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5545]) ).
fof(f5627,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,[],[f2540]) ).
fof(f5628,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,[],[f5627]) ).
fof(f5675,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2564]) ).
fof(f5676,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5675]) ).
fof(f5685,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,[],[f2569]) ).
fof(f5686,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,[],[f5685]) ).
fof(f5726,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,[],[f2597]) ).
fof(f5727,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,[],[f5726]) ).
fof(f5862,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f6041,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(f6042,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,[],[f6041]) ).
fof(f6073,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,[],[f2873]) ).
fof(f6074,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,[],[f6073]) ).
fof(f6075,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,[],[f2874]) ).
fof(f6076,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,[],[f6075]) ).
fof(f6095,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,[],[f2884]) ).
fof(f6096,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,[],[f6095]) ).
fof(f6133,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f2903]) ).
fof(f6134,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f6133]) ).
fof(f6135,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f2904]) ).
fof(f6136,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f6135]) ).
fof(f6147,plain,
! [X0,X1,X2] :
( m1_subset_1(k20_filter_2(X0,X1,X2),k1_zfmisc_1(u1_struct_0(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)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f2910]) ).
fof(f6148,plain,
! [X0,X1,X2] :
( m1_subset_1(k20_filter_2(X0,X1,X2),k1_zfmisc_1(u1_struct_0(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)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f6147]) ).
fof(f6210,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,[],[f2943]) ).
fof(f6211,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,[],[f6210]) ).
fof(f6254,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,[],[f2965]) ).
fof(f6255,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,[],[f6254]) ).
fof(f6258,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,[],[f2967]) ).
fof(f6259,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,[],[f6258]) ).
fof(f6278,plain,
! [X0,X1,X2] :
( ~ v1_xboole_0(k20_filter_2(X0,X1,X2))
| 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)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f2977]) ).
fof(f6279,plain,
! [X0,X1,X2] :
( ~ v1_xboole_0(k20_filter_2(X0,X1,X2))
| 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)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f6278]) ).
fof(f6282,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) )
| v1_xboole_0(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(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,[],[f2979]) ).
fof(f6283,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) )
| v1_xboole_0(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(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,[],[f6282]) ).
fof(f6290,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),k19_filter_2(X0,X1),X2)))
& r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,k19_filter_2(X0,X2)))) )
| 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,[],[f2983]) ).
fof(f6291,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),k19_filter_2(X0,X1),X2)))
& r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,k19_filter_2(X0,X2)))) )
| 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,[],[f6290]) ).
fof(f6296,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k20_filter_2(X0,X1,X2)))
& m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2987]) ).
fof(f6297,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k20_filter_2(X0,X1,X2)))
& m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f6296]) ).
fof(f6472,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP112(X0) ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f6473,plain,
! [X0] :
( sP112(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f5686,f6472]) ).
fof(f6504,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f3079]) ).
fof(f6505,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f6504]) ).
fof(f6506,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK127(X0,X1),X1)
& r2_hidden(sK127(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK127]),skolemize(X2,sK127(X0,X1))],[f6505]) ).
fof(f6542,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(f6543,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,[],[f6542]) ).
fof(f7874,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)) )
| ~ sP112(X0) ),
inference(nnf_transformation,[],[f6472]) ).
fof(f8000,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,[],[f6074]) ).
fof(f8037,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,[],[f6255]) ).
fof(f8038,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,[],[f8037]) ).
fof(f8039,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,[],[f8038]) ).
fof(f8040,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK1071(X0,X1,X2))
& r1_tarski(X1,sK1071(X0,X1,X2))
& m2_filter_2(sK1071(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,[sK1071]),skolemize(X3,sK1071(X0,X1,X2))],[f8039]) ).
fof(f8047,plain,
( ~ r1_filter_2(u1_struct_0(sK1076),k19_filter_2(sK1076,k4_subset_1(u1_struct_0(sK1076),sK1077,sK1078)),k19_filter_2(sK1076,k20_filter_2(sK1076,sK1077,sK1078)))
& m2_filter_2(sK1078,sK1076)
& m2_filter_2(sK1077,sK1076)
& ~ v3_struct_0(sK1076)
& v10_lattices(sK1076)
& l3_lattices(sK1076) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1076,sK1077,sK1078]),skolemize(X0,sK1076),skolemize(X1,sK1077),skolemize(X2,sK1078)],[f6297]) ).
fof(f8062,plain,
! [X0,X1] :
( r2_hidden(sK127(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f6506]) ).
fof(f8128,plain,
! [X0,X1] :
( r1_tarski(X1,X0)
| X0 != X1 ),
inference(cnf_transformation,[],[f6543]) ).
fof(f8175,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f3102]) ).
fof(f8180,plain,
! [X2,X0,X1] : k2_xboole_0(k2_xboole_0(X0,X1),X2) = k2_xboole_0(X0,k2_xboole_0(X1,X2)),
inference(cnf_transformation,[],[f73]) ).
fof(f8188,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = X1
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f3112]) ).
fof(f8229,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f8279,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k3_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f163]) ).
fof(f8417,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f8505,plain,
! [X0] : k3_tarski(k1_tarski(X0)) = X0,
inference(cnf_transformation,[],[f356]) ).
fof(f8593,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k3_tarski(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f418]) ).
fof(f8818,plain,
! [X2,X0,X1] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f3388]) ).
fof(f8819,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1) ),
inference(cnf_transformation,[],[f3390]) ).
fof(f8821,plain,
! [X2,X0,X1] :
( k2_xboole_0(X1,X2) = k4_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f3394]) ).
fof(f12604,plain,
! [X2,X0,X1] :
( ~ m1_filter_0(X2,X0)
| k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k5_filter_0(X0,X1,X2))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5546]) ).
fof(f12694,plain,
! [X0,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(cnf_transformation,[],[f5628]) ).
fof(f12743,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5676]) ).
fof(f12764,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP112(X0) ),
inference(cnf_transformation,[],[f7874]) ).
fof(f12773,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP112(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6473]) ).
fof(f12890,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5727]) ).
fof(f13011,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5862]) ).
fof(f13273,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,[],[f6042]) ).
fof(f13306,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,[],[f8000]) ).
fof(f13308,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6076]) ).
fof(f13309,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,[],[f6076]) ).
fof(f13320,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| k3_filter_0(X0,X1) = k3_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f6096]) ).
fof(f13341,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f6134]) ).
fof(f13342,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k7_filter_2(X0,X1) = k15_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f6136]) ).
fof(f13348,plain,
! [X2,X0,X1] :
( m1_subset_1(k20_filter_2(X0,X1,X2),k1_zfmisc_1(u1_struct_0(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)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f6148]) ).
fof(f13421,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,[],[f6211]) ).
fof(f13474,plain,
! [X2,X0,X1] :
( r1_tarski(X1,sK1071(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,[],[f8040]) ).
fof(f13475,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X2,sK1071(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,[],[f8040]) ).
fof(f13481,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X2)
| k19_filter_2(X0,X1) = k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
| 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,[],[f6259]) ).
fof(f13502,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(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)))
| v1_xboole_0(X2)
| ~ v1_xboole_0(k20_filter_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f6279]) ).
fof(f13507,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X4)
| k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(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(cnf_transformation,[],[f6283]) ).
fof(f13517,plain,
! [X2,X0,X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),k19_filter_2(X0,X1),X2)))
| 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(cnf_transformation,[],[f6291]) ).
fof(f13521,plain,
l3_lattices(sK1076),
inference(cnf_transformation,[],[f8047]) ).
fof(f13522,plain,
v10_lattices(sK1076),
inference(cnf_transformation,[],[f8047]) ).
fof(f13523,plain,
~ v3_struct_0(sK1076),
inference(cnf_transformation,[],[f8047]) ).
fof(f13524,plain,
m2_filter_2(sK1077,sK1076),
inference(cnf_transformation,[],[f8047]) ).
fof(f13525,plain,
m2_filter_2(sK1078,sK1076),
inference(cnf_transformation,[],[f8047]) ).
fof(f13526,plain,
~ r1_filter_2(u1_struct_0(sK1076),k19_filter_2(sK1076,k4_subset_1(u1_struct_0(sK1076),sK1077,sK1078)),k19_filter_2(sK1076,k20_filter_2(sK1076,sK1077,sK1078))),
inference(cnf_transformation,[],[f8047]) ).
fof(f13527,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(definition_unfolding,[],[f8279,f8229]) ).
fof(f13579,plain,
! [X2,X0,X1] : k5_xboole_0(k5_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),X2),k4_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),k4_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),X2))) = k5_xboole_0(k5_xboole_0(X0,k5_xboole_0(k5_xboole_0(X1,X2),k4_xboole_0(X1,k4_xboole_0(X1,X2)))),k4_xboole_0(X0,k4_xboole_0(X0,k5_xboole_0(k5_xboole_0(X1,X2),k4_xboole_0(X1,k4_xboole_0(X1,X2)))))),
inference(definition_unfolding,[],[f8180,f13527,f13527,f13527,f13527]) ).
fof(f13587,plain,
! [X0,X1] :
( k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))) = X1
| ~ r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f8188,f13527]) ).
fof(f13770,plain,
! [X0] : k3_tarski(k2_tarski(X0,X0)) = X0,
inference(definition_unfolding,[],[f8505,f8417]) ).
fof(f13841,plain,
! [X0,X1] : k3_tarski(k2_tarski(X0,X1)) = k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(definition_unfolding,[],[f8593,f13527]) ).
fof(f13921,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k4_subset_1(X0,X1,X2) = k5_xboole_0(k5_xboole_0(X1,X2),k4_xboole_0(X1,k4_xboole_0(X1,X2))) ),
inference(definition_unfolding,[],[f8821,f13527]) ).
fof(f14896,plain,
! [X1] : r1_tarski(X1,X1),
inference(equality_resolution,[],[f8128]) ).
fof(f15452,definition,
sF1079 = u1_struct_0(sK1076),
introduced(definition,[new_symbols(definition,[sF1079])],[function_definition]) ).
fof(f15453,plain,
u1_struct_0(sK1076) = sF1079,
inference(reorient_equations,[],[f15452]) ).
fof(f15454,definition,
sF1080 = k4_subset_1(sF1079,sK1077,sK1078),
introduced(definition,[new_symbols(definition,[sF1080])],[function_definition]) ).
fof(f15455,plain,
k4_subset_1(sF1079,sK1077,sK1078) = sF1080,
inference(reorient_equations,[],[f15454]) ).
fof(f15456,definition,
sF1081 = k19_filter_2(sK1076,sF1080),
introduced(definition,[new_symbols(definition,[sF1081])],[function_definition]) ).
fof(f15457,plain,
k19_filter_2(sK1076,sF1080) = sF1081,
inference(reorient_equations,[],[f15456]) ).
fof(f15458,definition,
sF1082 = k20_filter_2(sK1076,sK1077,sK1078),
introduced(definition,[new_symbols(definition,[sF1082])],[function_definition]) ).
fof(f15459,plain,
k20_filter_2(sK1076,sK1077,sK1078) = sF1082,
inference(reorient_equations,[],[f15458]) ).
fof(f15460,definition,
sF1083 = k19_filter_2(sK1076,sF1082),
introduced(definition,[new_symbols(definition,[sF1083])],[function_definition]) ).
fof(f15461,plain,
k19_filter_2(sK1076,sF1082) = sF1083,
inference(reorient_equations,[],[f15460]) ).
fof(f15462,plain,
~ r1_filter_2(sF1079,sF1081,sF1083),
inference(definition_folding,[],[f13526,f15461,f15459,f15457,f15455,f15453,f15453]) ).
fof(f17317,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| k3_tarski(k2_tarski(X0,X1)) = X1 ),
inference(forward_demodulation,[],[f13587,f13841]) ).
fof(f17325,plain,
! [X2,X0,X1] : k5_xboole_0(k5_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),X2),k4_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),k4_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),X2))) = k3_tarski(k2_tarski(X0,k5_xboole_0(k5_xboole_0(X1,X2),k4_xboole_0(X1,k4_xboole_0(X1,X2))))),
inference(forward_demodulation,[],[f13579,f13841]) ).
fof(f17549,plain,
! [X2,X0,X1] : k5_xboole_0(k5_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),X2),k4_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),k4_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),X2))) = k3_tarski(k2_tarski(X0,k3_tarski(k2_tarski(X1,X2)))),
inference(forward_demodulation,[],[f17325,f13841]) ).
fof(f17660,plain,
! [X2,X0,X1] : k3_tarski(k2_tarski(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),X2)) = k3_tarski(k2_tarski(X0,k3_tarski(k2_tarski(X1,X2)))),
inference(forward_demodulation,[],[f17549,f13841]) ).
fof(f17739,plain,
! [X2,X0,X1] : k3_tarski(k2_tarski(k3_tarski(k2_tarski(X0,X1)),X2)) = k3_tarski(k2_tarski(X0,k3_tarski(k2_tarski(X1,X2)))),
inference(forward_demodulation,[],[f17660,f13841]) ).
fof(f18067,plain,
( ~ v1_xboole_0(sK1077)
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(resolution,[],[f13309,f13524]) ).
fof(f18068,plain,
( ~ v1_xboole_0(sK1078)
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(resolution,[],[f13309,f13525]) ).
fof(f18080,plain,
( v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| k7_filter_2(sK1076,sK1077) = k15_filter_2(sK1076,sK1077) ),
inference(resolution,[],[f13342,f13524]) ).
fof(f18081,plain,
( v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| k7_filter_2(sK1076,sK1078) = k15_filter_2(sK1076,sK1078) ),
inference(resolution,[],[f13342,f13525]) ).
fof(f18085,plain,
( m2_lattice4(sK1077,sK1076)
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(resolution,[],[f13308,f13524]) ).
fof(f18086,plain,
( m2_lattice4(sK1078,sK1076)
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(resolution,[],[f13308,f13525]) ).
fof(f18090,plain,
( v3_struct_0(sK1076)
| u1_struct_0(sK1076) = u1_struct_0(k1_lattice2(sK1076)) ),
inference(resolution,[],[f12890,f13521]) ).
fof(f18091,plain,
u1_struct_0(sK1076) = u1_struct_0(k1_lattice2(sK1076)),
inference(forward_subsumption_resolution,[],[f18090,f13523]) ).
fof(f18092,plain,
sF1079 = u1_struct_0(k1_lattice2(sK1076)),
inference(forward_demodulation,[],[f18091,f15453]) ).
fof(f18105,plain,
( m1_subset_1(sF1080,k1_zfmisc_1(sF1079))
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079)) ),
inference(superposition,[],[f8818,f15455]) ).
fof(f18107,definition,
( spl1084_345
<=> m1_subset_1(sK1078,k1_zfmisc_1(sF1079)) ),
introduced(definition,[new_symbols(definition,[spl1084_345])],[avatar_definition]) ).
fof(f18108,plain,
( m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| ~ spl1084_345 ),
inference(avatar_component_clause,[],[f18107]) ).
fof(f18109,plain,
( ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| spl1084_345 ),
inference(avatar_component_clause,[],[f18107]) ).
fof(f18111,definition,
( spl1084_346
<=> m1_subset_1(sK1077,k1_zfmisc_1(sF1079)) ),
introduced(definition,[new_symbols(definition,[spl1084_346])],[avatar_definition]) ).
fof(f18112,plain,
( m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| ~ spl1084_346 ),
inference(avatar_component_clause,[],[f18111]) ).
fof(f18113,plain,
( ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| spl1084_346 ),
inference(avatar_component_clause,[],[f18111]) ).
fof(f18115,definition,
( spl1084_347
<=> m1_subset_1(sF1080,k1_zfmisc_1(sF1079)) ),
introduced(definition,[new_symbols(definition,[spl1084_347])],[avatar_definition]) ).
fof(f18117,plain,
( m1_subset_1(sF1080,k1_zfmisc_1(sF1079))
| ~ spl1084_347 ),
inference(avatar_component_clause,[],[f18115]) ).
fof(f18118,plain,
( ~ spl1084_345
| ~ spl1084_346
| spl1084_347 ),
inference(avatar_split_clause,[],[f18105,f18115,f18111,f18107]) ).
fof(f18126,plain,
! [X0,X1] :
( m1_subset_1(k20_filter_2(sK1076,X0,X1),k1_zfmisc_1(sF1079))
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079)) ),
inference(superposition,[],[f13348,f15453]) ).
fof(f18140,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,[],[f13474,f13475]) ).
fof(f18141,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,[],[f18140]) ).
fof(f18142,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| ~ 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,[],[f18141,f13309]) ).
fof(f18148,plain,
! [X0,X1] :
( r1_filter_2(sF1079,k19_filter_2(sK1076,k4_subset_1(sF1079,X0,X1)),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,X0),X1)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(superposition,[],[f13517,f15453]) ).
fof(f18162,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ m1_filter_0(X0,k1_lattice2(sK1076))
| v3_struct_0(k1_lattice2(sK1076))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076)) ),
inference(superposition,[],[f12694,f18092]) ).
fof(f18173,definition,
( spl1084_349
<=> v3_struct_0(k1_lattice2(sK1076)) ),
introduced(definition,[new_symbols(definition,[spl1084_349])],[avatar_definition]) ).
fof(f18174,plain,
( ~ v3_struct_0(k1_lattice2(sK1076))
| spl1084_349 ),
inference(avatar_component_clause,[],[f18173]) ).
fof(f18175,plain,
( v3_struct_0(k1_lattice2(sK1076))
| ~ spl1084_349 ),
inference(avatar_component_clause,[],[f18173]) ).
fof(f18230,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ m2_lattice4(X0,sK1076)
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(superposition,[],[f13273,f15453]) ).
fof(f18253,plain,
( v3_struct_0(sK1076)
| sP112(sK1076)
| ~ l3_lattices(sK1076) ),
inference(resolution,[],[f12773,f13522]) ).
fof(f18254,plain,
( sP112(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18253,f13523]) ).
fof(f18255,plain,
sP112(sK1076),
inference(forward_subsumption_resolution,[],[f18254,f13521]) ).
fof(f18296,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| k7_filter_2(sK1076,X0) = X0
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(superposition,[],[f13421,f15453]) ).
fof(f18391,plain,
( ~ v1_xboole_0(sK1078)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18068,f13523]) ).
fof(f18392,plain,
( ~ v1_xboole_0(sK1077)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18067,f13523]) ).
fof(f18398,plain,
( ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| k7_filter_2(sK1076,sK1078) = k15_filter_2(sK1076,sK1078) ),
inference(forward_subsumption_resolution,[],[f18081,f13523]) ).
fof(f18399,plain,
( ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| k7_filter_2(sK1076,sK1077) = k15_filter_2(sK1076,sK1077) ),
inference(forward_subsumption_resolution,[],[f18080,f13523]) ).
fof(f18401,plain,
( m2_lattice4(sK1078,sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18086,f13523]) ).
fof(f18402,plain,
( m2_lattice4(sK1077,sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18085,f13523]) ).
fof(f18404,definition,
( spl1084_356
<=> l3_lattices(k1_lattice2(sK1076)) ),
introduced(definition,[new_symbols(definition,[spl1084_356])],[avatar_definition]) ).
fof(f18405,plain,
( l3_lattices(k1_lattice2(sK1076))
| ~ spl1084_356 ),
inference(avatar_component_clause,[],[f18404]) ).
fof(f18406,plain,
( ~ l3_lattices(k1_lattice2(sK1076))
| spl1084_356 ),
inference(avatar_component_clause,[],[f18404]) ).
fof(f18408,definition,
( spl1084_357
<=> v10_lattices(k1_lattice2(sK1076)) ),
introduced(definition,[new_symbols(definition,[spl1084_357])],[avatar_definition]) ).
fof(f18409,plain,
( v10_lattices(k1_lattice2(sK1076))
| ~ spl1084_357 ),
inference(avatar_component_clause,[],[f18408]) ).
fof(f18410,plain,
( ~ v10_lattices(k1_lattice2(sK1076))
| spl1084_357 ),
inference(avatar_component_clause,[],[f18408]) ).
fof(f18450,plain,
! [X0,X1] :
( m1_subset_1(k20_filter_2(sK1076,X0,X1),k1_zfmisc_1(sF1079))
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079)) ),
inference(forward_subsumption_resolution,[],[f18126,f13523]) ).
fof(f18456,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f18142,f14896]) ).
fof(f18473,plain,
! [X0,X1] :
( r1_filter_2(sF1079,k19_filter_2(sK1076,k4_subset_1(sF1079,X0,X1)),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,X0),X1)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18148,f13523]) ).
fof(f18484,definition,
( spl1084_370
<=> ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ m1_filter_0(X0,k1_lattice2(sK1076)) ) ),
introduced(definition,[new_symbols(definition,[spl1084_370])],[avatar_definition]) ).
fof(f18485,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK1076))
| m1_subset_1(X0,k1_zfmisc_1(sF1079)) )
| ~ spl1084_370 ),
inference(avatar_component_clause,[],[f18484]) ).
fof(f18486,plain,
( ~ spl1084_356
| ~ spl1084_357
| spl1084_349
| spl1084_370 ),
inference(avatar_split_clause,[],[f18162,f18484,f18173,f18408,f18404]) ).
fof(f18508,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ m2_lattice4(X0,sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18230,f13523]) ).
fof(f18547,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| k7_filter_2(sK1076,X0) = X0
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18296,f13523]) ).
fof(f18594,plain,
( ~ v1_xboole_0(sK1078)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18391,f13522]) ).
fof(f18595,plain,
( ~ v1_xboole_0(sK1077)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18392,f13522]) ).
fof(f18601,plain,
( ~ l3_lattices(sK1076)
| k7_filter_2(sK1076,sK1078) = k15_filter_2(sK1076,sK1078) ),
inference(forward_subsumption_resolution,[],[f18398,f13522]) ).
fof(f18602,plain,
( ~ l3_lattices(sK1076)
| k7_filter_2(sK1076,sK1077) = k15_filter_2(sK1076,sK1077) ),
inference(forward_subsumption_resolution,[],[f18399,f13522]) ).
fof(f18604,plain,
( m2_lattice4(sK1078,sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18401,f13522]) ).
fof(f18605,plain,
( m2_lattice4(sK1077,sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18402,f13522]) ).
fof(f18610,plain,
! [X0,X1] :
( m1_subset_1(k20_filter_2(sK1076,X0,X1),k1_zfmisc_1(sF1079))
| ~ l3_lattices(sK1076)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079)) ),
inference(forward_subsumption_resolution,[],[f18450,f13522]) ).
fof(f18615,plain,
! [X0,X1] :
( r1_filter_2(sF1079,k19_filter_2(sK1076,k4_subset_1(sF1079,X0,X1)),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,X0),X1)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18473,f13522]) ).
fof(f18637,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ m2_lattice4(X0,sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18508,f13522]) ).
fof(f18652,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| k7_filter_2(sK1076,X0) = X0
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f18547,f13522]) ).
fof(f18668,plain,
~ v1_xboole_0(sK1078),
inference(forward_subsumption_resolution,[],[f18594,f13521]) ).
fof(f18669,plain,
~ v1_xboole_0(sK1077),
inference(forward_subsumption_resolution,[],[f18595,f13521]) ).
fof(f18675,plain,
k7_filter_2(sK1076,sK1078) = k15_filter_2(sK1076,sK1078),
inference(forward_subsumption_resolution,[],[f18601,f13521]) ).
fof(f18676,plain,
k7_filter_2(sK1076,sK1077) = k15_filter_2(sK1076,sK1077),
inference(forward_subsumption_resolution,[],[f18602,f13521]) ).
fof(f18678,plain,
m2_lattice4(sK1078,sK1076),
inference(forward_subsumption_resolution,[],[f18604,f13521]) ).
fof(f18679,plain,
m2_lattice4(sK1077,sK1076),
inference(forward_subsumption_resolution,[],[f18605,f13521]) ).
fof(f18683,plain,
! [X0,X1] :
( m1_subset_1(k20_filter_2(sK1076,X0,X1),k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079)) ),
inference(forward_subsumption_resolution,[],[f18610,f13521]) ).
fof(f18688,plain,
! [X0,X1] :
( r1_filter_2(sF1079,k19_filter_2(sK1076,k4_subset_1(sF1079,X0,X1)),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,X0),X1)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079)) ),
inference(forward_subsumption_resolution,[],[f18615,f13521]) ).
fof(f18705,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ m2_lattice4(X0,sK1076) ),
inference(forward_subsumption_resolution,[],[f18637,f13521]) ).
fof(f18719,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| k7_filter_2(sK1076,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f18652,f13521]) ).
fof(f18780,definition,
( spl1084_386
<=> v1_xboole_0(sF1082) ),
introduced(definition,[new_symbols(definition,[spl1084_386])],[avatar_definition]) ).
fof(f18781,plain,
( ~ v1_xboole_0(sF1082)
| spl1084_386 ),
inference(avatar_component_clause,[],[f18780]) ).
fof(f18782,plain,
( v1_xboole_0(sF1082)
| ~ spl1084_386 ),
inference(avatar_component_clause,[],[f18780]) ).
fof(f18792,definition,
( spl1084_389
<=> m1_subset_1(sF1082,k1_zfmisc_1(sF1079)) ),
introduced(definition,[new_symbols(definition,[spl1084_389])],[avatar_definition]) ).
fof(f18793,plain,
( m1_subset_1(sF1082,k1_zfmisc_1(sF1079))
| ~ spl1084_389 ),
inference(avatar_component_clause,[],[f18792]) ).
fof(f18794,plain,
( ~ m1_subset_1(sF1082,k1_zfmisc_1(sF1079))
| spl1084_389 ),
inference(avatar_component_clause,[],[f18792]) ).
fof(f18797,definition,
( spl1084_390
<=> v1_xboole_0(sF1080) ),
introduced(definition,[new_symbols(definition,[spl1084_390])],[avatar_definition]) ).
fof(f18798,plain,
( ~ v1_xboole_0(sF1080)
| spl1084_390 ),
inference(avatar_component_clause,[],[f18797]) ).
fof(f18799,plain,
( v1_xboole_0(sF1080)
| ~ spl1084_390 ),
inference(avatar_component_clause,[],[f18797]) ).
fof(f18862,definition,
( spl1084_403
<=> m1_subset_1(k4_subset_1(sF1079,sK1078,sK1077),k1_zfmisc_1(sF1079)) ),
introduced(definition,[new_symbols(definition,[spl1084_403])],[avatar_definition]) ).
fof(f18863,plain,
( m1_subset_1(k4_subset_1(sF1079,sK1078,sK1077),k1_zfmisc_1(sF1079))
| ~ spl1084_403 ),
inference(avatar_component_clause,[],[f18862]) ).
fof(f18864,plain,
( ~ m1_subset_1(k4_subset_1(sF1079,sK1078,sK1077),k1_zfmisc_1(sF1079))
| spl1084_403 ),
inference(avatar_component_clause,[],[f18862]) ).
fof(f19022,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f18456,f13273]) ).
fof(f19027,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_lattice4(X0,X1) ),
inference(duplicate_literal_removal,[],[f19022]) ).
fof(f19030,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f19027,f13308]) ).
fof(f19038,plain,
( ~ m2_lattice4(sK1078,sK1076)
| spl1084_345 ),
inference(resolution,[],[f18705,f18109]) ).
fof(f19039,plain,
( $false
| spl1084_345 ),
inference(forward_subsumption_resolution,[],[f19038,f18678]) ).
fof(f19040,plain,
spl1084_345,
inference(avatar_contradiction_clause,[],[f19039]) ).
fof(f19049,plain,
( ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| spl1084_403 ),
inference(resolution,[],[f18864,f8818]) ).
fof(f19057,plain,
( m1_filter_2(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076))
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| ~ m2_filter_2(sK1078,sK1076) ),
inference(superposition,[],[f13341,f18675]) ).
fof(f19058,plain,
( m1_filter_2(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076))
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| ~ m2_filter_2(sK1078,sK1076) ),
inference(forward_subsumption_resolution,[],[f19057,f13523]) ).
fof(f19060,plain,
( m1_filter_2(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076))
| ~ l3_lattices(sK1076)
| ~ m2_filter_2(sK1078,sK1076) ),
inference(forward_subsumption_resolution,[],[f19058,f13522]) ).
fof(f19062,plain,
( m1_filter_2(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076))
| ~ m2_filter_2(sK1078,sK1076) ),
inference(forward_subsumption_resolution,[],[f19060,f13521]) ).
fof(f19064,plain,
m1_filter_2(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076)),
inference(forward_subsumption_resolution,[],[f19062,f13525]) ).
fof(f19076,plain,
( m1_filter_2(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076))
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| ~ m2_filter_2(sK1077,sK1076) ),
inference(superposition,[],[f13341,f18676]) ).
fof(f19077,plain,
( m1_filter_2(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076))
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| ~ m2_filter_2(sK1077,sK1076) ),
inference(forward_subsumption_resolution,[],[f19076,f13523]) ).
fof(f19079,plain,
( m1_filter_2(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076))
| ~ l3_lattices(sK1076)
| ~ m2_filter_2(sK1077,sK1076) ),
inference(forward_subsumption_resolution,[],[f19077,f13522]) ).
fof(f19081,plain,
( m1_filter_2(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076))
| ~ m2_filter_2(sK1077,sK1076) ),
inference(forward_subsumption_resolution,[],[f19079,f13521]) ).
fof(f19083,plain,
m1_filter_2(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076)),
inference(forward_subsumption_resolution,[],[f19081,f13524]) ).
fof(f19101,plain,
( sK1077 = k19_filter_2(sK1076,sK1077)
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(resolution,[],[f19030,f13524]) ).
fof(f19110,plain,
( sK1077 = k19_filter_2(sK1076,sK1077)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f19101,f13523]) ).
fof(f19113,plain,
( sK1077 = k19_filter_2(sK1076,sK1077)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f19110,f13522]) ).
fof(f19116,plain,
sK1077 = k19_filter_2(sK1076,sK1077),
inference(forward_subsumption_resolution,[],[f19113,f13521]) ).
fof(f19308,plain,
( ~ l3_lattices(sK1076)
| spl1084_356 ),
inference(resolution,[],[f18406,f13011]) ).
fof(f19309,plain,
( $false
| spl1084_356 ),
inference(forward_subsumption_resolution,[],[f19308,f13521]) ).
fof(f19310,plain,
spl1084_356,
inference(avatar_contradiction_clause,[],[f19309]) ).
fof(f19322,plain,
( ~ sP112(sK1076)
| spl1084_357 ),
inference(resolution,[],[f18410,f12764]) ).
fof(f19323,plain,
( $false
| spl1084_357 ),
inference(forward_subsumption_resolution,[],[f19322,f18255]) ).
fof(f19324,plain,
spl1084_357,
inference(avatar_contradiction_clause,[],[f19323]) ).
fof(f19335,plain,
( m1_subset_1(sF1082,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1077)
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079)) ),
inference(superposition,[],[f18683,f15459]) ).
fof(f19359,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| k4_subset_1(sF1079,X0,sK1078) = k4_subset_1(sF1079,sK1078,X0) )
| ~ spl1084_345 ),
inference(resolution,[],[f18108,f8819]) ).
fof(f19363,plain,
( v3_struct_0(sK1076)
| ~ l3_lattices(sK1076)
| ~ spl1084_349 ),
inference(resolution,[],[f18175,f12743]) ).
fof(f19364,plain,
( ~ l3_lattices(sK1076)
| ~ spl1084_349 ),
inference(forward_subsumption_resolution,[],[f19363,f13523]) ).
fof(f19365,plain,
( $false
| ~ spl1084_349 ),
inference(forward_subsumption_resolution,[],[f19364,f13521]) ).
fof(f19366,plain,
~ spl1084_349,
inference(avatar_contradiction_clause,[],[f19365]) ).
fof(f19444,plain,
( m1_filter_0(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076))
| v3_struct_0(k1_lattice2(sK1076))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076)) ),
inference(resolution,[],[f19083,f13306]) ).
fof(f19445,plain,
( m1_filter_0(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076))
| spl1084_349 ),
inference(forward_subsumption_resolution,[],[f19444,f18174]) ).
fof(f19449,plain,
( m1_filter_0(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076))
| spl1084_349
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f19445,f18409]) ).
fof(f19453,plain,
( m1_filter_0(k7_filter_2(sK1076,sK1077),k1_lattice2(sK1076))
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f19449,f18405]) ).
fof(f19460,plain,
! [X0] :
( ~ m2_lattice4(X0,sK1076)
| k7_filter_2(sK1076,X0) = X0 ),
inference(resolution,[],[f18719,f18705]) ).
fof(f19463,plain,
( sK1078 = k7_filter_2(sK1076,sK1078)
| ~ spl1084_345 ),
inference(resolution,[],[f18719,f18108]) ).
fof(f19493,plain,
( m1_filter_0(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076))
| v3_struct_0(k1_lattice2(sK1076))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076)) ),
inference(resolution,[],[f19064,f13306]) ).
fof(f19495,plain,
( m1_filter_0(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076))
| spl1084_349 ),
inference(forward_subsumption_resolution,[],[f19493,f18174]) ).
fof(f19499,plain,
( m1_filter_0(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076))
| spl1084_349
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f19495,f18409]) ).
fof(f19503,plain,
( m1_filter_0(k7_filter_2(sK1076,sK1078),k1_lattice2(sK1076))
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f19499,f18405]) ).
fof(f19507,plain,
( m1_filter_0(sK1078,k1_lattice2(sK1076))
| ~ spl1084_345
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_demodulation,[],[f19503,f19463]) ).
fof(f19513,plain,
( ! [X0] :
( k3_filter_0(k1_lattice2(sK1076),k4_subset_1(u1_struct_0(k1_lattice2(sK1076)),X0,sK1078)) = k3_filter_0(k1_lattice2(sK1076),k5_filter_0(k1_lattice2(sK1076),X0,sK1078))
| ~ m1_filter_0(X0,k1_lattice2(sK1076))
| v3_struct_0(k1_lattice2(sK1076))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076)) )
| ~ spl1084_345
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(resolution,[],[f19507,f12604]) ).
fof(f19516,plain,
( ! [X0] :
( k3_filter_0(k1_lattice2(sK1076),k4_subset_1(u1_struct_0(k1_lattice2(sK1076)),X0,sK1078)) = k3_filter_0(k1_lattice2(sK1076),k5_filter_0(k1_lattice2(sK1076),X0,sK1078))
| ~ m1_filter_0(X0,k1_lattice2(sK1076))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076)) )
| ~ spl1084_345
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f19513,f18174]) ).
fof(f19518,plain,
( ! [X0] :
( k3_filter_0(k1_lattice2(sK1076),k4_subset_1(u1_struct_0(k1_lattice2(sK1076)),X0,sK1078)) = k3_filter_0(k1_lattice2(sK1076),k5_filter_0(k1_lattice2(sK1076),X0,sK1078))
| ~ m1_filter_0(X0,k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076)) )
| ~ spl1084_345
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f19516,f18409]) ).
fof(f19520,plain,
( ! [X0] :
( k3_filter_0(k1_lattice2(sK1076),k4_subset_1(u1_struct_0(k1_lattice2(sK1076)),X0,sK1078)) = k3_filter_0(k1_lattice2(sK1076),k5_filter_0(k1_lattice2(sK1076),X0,sK1078))
| ~ m1_filter_0(X0,k1_lattice2(sK1076)) )
| ~ spl1084_345
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f19518,f18405]) ).
fof(f19522,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK1076))
| k3_filter_0(k1_lattice2(sK1076),k5_filter_0(k1_lattice2(sK1076),X0,sK1078)) = k3_filter_0(k1_lattice2(sK1076),k4_subset_1(sF1079,X0,sK1078)) )
| ~ spl1084_345
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_demodulation,[],[f19520,f18092]) ).
fof(f19610,plain,
( r1_filter_2(sF1079,k19_filter_2(sK1076,sF1080),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,sK1077),sK1078)))
| v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1077)
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079)) ),
inference(superposition,[],[f18688,f15455]) ).
fof(f19658,plain,
sK1077 = k7_filter_2(sK1076,sK1077),
inference(resolution,[],[f19460,f18679]) ).
fof(f19660,plain,
( m1_filter_0(sK1077,k1_lattice2(sK1076))
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(superposition,[],[f19453,f19658]) ).
fof(f19743,plain,
( m1_subset_1(k7_filter_2(sK1076,sK1077),k1_zfmisc_1(sF1079))
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| ~ spl1084_370 ),
inference(resolution,[],[f18485,f19453]) ).
fof(f19751,plain,
( m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| ~ spl1084_370 ),
inference(forward_demodulation,[],[f19743,f19658]) ).
fof(f19754,plain,
( $false
| spl1084_346
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| ~ spl1084_370 ),
inference(forward_subsumption_resolution,[],[f19751,f18113]) ).
fof(f19755,plain,
( spl1084_346
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| ~ spl1084_370 ),
inference(avatar_contradiction_clause,[],[f19754]) ).
fof(f19769,plain,
( ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| ~ spl1084_345
| spl1084_403 ),
inference(forward_subsumption_resolution,[],[f19049,f18108]) ).
fof(f19775,plain,
( v1_xboole_0(sK1077)
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| spl1084_389 ),
inference(forward_subsumption_resolution,[],[f19335,f18794]) ).
fof(f19780,plain,
( r1_filter_2(sF1079,k19_filter_2(sK1076,sF1080),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,sK1077),sK1078)))
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1077)
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079)) ),
inference(forward_subsumption_resolution,[],[f19610,f18668]) ).
fof(f19787,plain,
( $false
| ~ spl1084_345
| ~ spl1084_346
| spl1084_403 ),
inference(forward_subsumption_resolution,[],[f19769,f18112]) ).
fof(f19788,plain,
( ~ spl1084_345
| ~ spl1084_346
| spl1084_403 ),
inference(avatar_contradiction_clause,[],[f19787]) ).
fof(f19792,plain,
( ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| spl1084_389 ),
inference(forward_subsumption_resolution,[],[f19775,f18669]) ).
fof(f19796,plain,
( r1_filter_2(sF1079,k19_filter_2(sK1076,sF1080),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,sK1077),sK1078)))
| v1_xboole_0(sK1077)
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| ~ spl1084_345 ),
inference(forward_subsumption_resolution,[],[f19780,f18108]) ).
fof(f19803,plain,
( v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| ~ spl1084_346
| spl1084_389 ),
inference(forward_subsumption_resolution,[],[f19792,f18112]) ).
fof(f19806,plain,
( r1_filter_2(sF1079,k19_filter_2(sK1076,sF1080),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,sK1077),sK1078)))
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| ~ spl1084_345 ),
inference(forward_subsumption_resolution,[],[f19796,f18669]) ).
fof(f19810,plain,
( ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| ~ spl1084_346
| spl1084_389 ),
inference(forward_subsumption_resolution,[],[f19803,f18668]) ).
fof(f19813,plain,
( r1_filter_2(sF1079,k19_filter_2(sK1076,sF1080),k19_filter_2(sK1076,k4_subset_1(sF1079,k19_filter_2(sK1076,sK1077),sK1078)))
| ~ spl1084_345
| ~ spl1084_346 ),
inference(forward_subsumption_resolution,[],[f19806,f18112]) ).
fof(f19817,plain,
( $false
| ~ spl1084_345
| ~ spl1084_346
| spl1084_389 ),
inference(forward_subsumption_resolution,[],[f19810,f18108]) ).
fof(f19818,plain,
( ~ spl1084_345
| ~ spl1084_346
| spl1084_389 ),
inference(avatar_contradiction_clause,[],[f19817]) ).
fof(f19820,plain,
( r1_filter_2(sF1079,k19_filter_2(sK1076,sF1080),k19_filter_2(sK1076,k4_subset_1(sF1079,sK1077,sK1078)))
| ~ spl1084_345
| ~ spl1084_346 ),
inference(forward_demodulation,[],[f19813,f19116]) ).
fof(f19824,plain,
( r1_filter_2(sF1079,k19_filter_2(sK1076,sF1080),k19_filter_2(sK1076,sF1080))
| ~ spl1084_345
| ~ spl1084_346 ),
inference(forward_demodulation,[],[f19820,f15455]) ).
fof(f19827,plain,
( r1_filter_2(sF1079,sF1081,sF1081)
| ~ spl1084_345
| ~ spl1084_346 ),
inference(forward_demodulation,[],[f19824,f15457]) ).
fof(f19833,plain,
( sF1082 = k7_filter_2(sK1076,sF1082)
| ~ spl1084_389 ),
inference(resolution,[],[f18793,f18719]) ).
fof(f19870,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| k4_subset_1(sF1079,X0,sK1077) = k5_xboole_0(k5_xboole_0(X0,sK1077),k4_xboole_0(X0,k4_xboole_0(X0,sK1077))) )
| ~ spl1084_346 ),
inference(resolution,[],[f18112,f13921]) ).
fof(f19874,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| k4_subset_1(sF1079,X0,sK1077) = k3_tarski(k2_tarski(X0,sK1077)) )
| ~ spl1084_346 ),
inference(forward_demodulation,[],[f19870,f13841]) ).
fof(f19928,plain,
( sF1080 = k7_filter_2(sK1076,sF1080)
| ~ spl1084_347 ),
inference(resolution,[],[f18117,f18719]) ).
fof(f20472,plain,
( k3_filter_0(k1_lattice2(sK1076),k5_filter_0(k1_lattice2(sK1076),sK1077,sK1078)) = k3_filter_0(k1_lattice2(sK1076),k4_subset_1(sF1079,sK1077,sK1078))
| ~ spl1084_345
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(resolution,[],[f19522,f19660]) ).
fof(f20475,plain,
( k3_filter_0(k1_lattice2(sK1076),k5_filter_0(k1_lattice2(sK1076),sK1077,sK1078)) = k3_filter_0(k1_lattice2(sK1076),sF1080)
| ~ spl1084_345
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_demodulation,[],[f20472,f15455]) ).
fof(f20865,plain,
( k4_subset_1(sF1079,k4_subset_1(sF1079,sK1078,sK1077),sK1077) = k3_tarski(k2_tarski(k4_subset_1(sF1079,sK1078,sK1077),sK1077))
| ~ spl1084_346
| ~ spl1084_403 ),
inference(resolution,[],[f19874,f18863]) ).
fof(f20871,plain,
( k4_subset_1(sF1079,sK1078,sK1077) = k3_tarski(k2_tarski(sK1078,sK1077))
| ~ spl1084_345
| ~ spl1084_346 ),
inference(resolution,[],[f19874,f18108]) ).
fof(f20873,plain,
( k4_subset_1(sF1079,sF1080,sK1077) = k3_tarski(k2_tarski(sF1080,sK1077))
| ~ spl1084_346
| ~ spl1084_347 ),
inference(resolution,[],[f19874,f18117]) ).
fof(f20877,plain,
( k4_subset_1(sF1079,k3_tarski(k2_tarski(sK1078,sK1077)),sK1077) = k3_tarski(k2_tarski(k3_tarski(k2_tarski(sK1078,sK1077)),sK1077))
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_403 ),
inference(forward_demodulation,[],[f20865,f20871]) ).
fof(f20878,plain,
( k4_subset_1(sF1079,k3_tarski(k2_tarski(sK1078,sK1077)),sK1077) = k3_tarski(k2_tarski(sK1078,k3_tarski(k2_tarski(sK1077,sK1077))))
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_403 ),
inference(forward_demodulation,[],[f20877,f17739]) ).
fof(f20879,plain,
( k3_tarski(k2_tarski(sK1078,sK1077)) = k4_subset_1(sF1079,k3_tarski(k2_tarski(sK1078,sK1077)),sK1077)
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_403 ),
inference(forward_demodulation,[],[f20878,f13770]) ).
fof(f21786,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ v1_xboole_0(X0) ),
inference(resolution,[],[f8175,f8062]) ).
fof(f22491,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v3_struct_0(k1_lattice2(sK1076))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1076),X0) = k3_filter_2(k1_lattice2(sK1076),X0) ),
inference(superposition,[],[f13320,f18092]) ).
fof(f22496,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ v10_lattices(k1_lattice2(sK1076))
| ~ l3_lattices(k1_lattice2(sK1076))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1076),X0) = k3_filter_2(k1_lattice2(sK1076),X0) )
| spl1084_349 ),
inference(forward_subsumption_resolution,[],[f22491,f18174]) ).
fof(f22500,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ l3_lattices(k1_lattice2(sK1076))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1076),X0) = k3_filter_2(k1_lattice2(sK1076),X0) )
| spl1084_349
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f22496,f18409]) ).
fof(f22502,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1076),X0) = k3_filter_2(k1_lattice2(sK1076),X0) )
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(forward_subsumption_resolution,[],[f22500,f18405]) ).
fof(f22557,plain,
( v1_xboole_0(sF1080)
| k3_filter_0(k1_lattice2(sK1076),sF1080) = k3_filter_2(k1_lattice2(sK1076),sF1080)
| ~ spl1084_347
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357 ),
inference(resolution,[],[f22502,f18117]) ).
fof(f22558,plain,
( v1_xboole_0(sF1082)
| k3_filter_0(k1_lattice2(sK1076),sF1082) = k3_filter_2(k1_lattice2(sK1076),sF1082)
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| ~ spl1084_389 ),
inference(resolution,[],[f22502,f18793]) ).
fof(f22703,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k20_filter_2(sK1076,X1,X2) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X1),k7_filter_2(sK1076,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF1079))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK1076)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076)))
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(superposition,[],[f13507,f18092]) ).
fof(f22706,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k20_filter_2(sK1076,X1,X2) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X1),k7_filter_2(sK1076,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF1079))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK1076)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076)))
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f22703,f13523]) ).
fof(f22710,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k20_filter_2(sK1076,X1,X2) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X1),k7_filter_2(sK1076,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF1079))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK1076)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076)))
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f22706,f13522]) ).
fof(f22714,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k20_filter_2(sK1076,X1,X2) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X1),k7_filter_2(sK1076,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF1079))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK1076)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076))) ),
inference(forward_subsumption_resolution,[],[f22710,f13521]) ).
fof(f22717,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(sF1079))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k20_filter_2(sK1076,X1,X2) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X1),k7_filter_2(sK1076,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF1079))
| v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076))) ),
inference(forward_demodulation,[],[f22714,f15453]) ).
fof(f22719,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| ~ m1_subset_1(X2,k1_zfmisc_1(sF1079))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k20_filter_2(sK1076,X1,X2) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X1),k7_filter_2(sK1076,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF1079))
| v1_xboole_0(X2)
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f22717,f15453]) ).
fof(f22721,definition,
( spl1084_496
<=> ! [X3] :
( v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF1079)) ) ),
introduced(definition,[new_symbols(definition,[spl1084_496])],[avatar_definition]) ).
fof(f22722,plain,
( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(sF1079))
| v1_xboole_0(X3) )
| ~ spl1084_496 ),
inference(avatar_component_clause,[],[f22721]) ).
fof(f22728,definition,
( spl1084_498
<=> ! [X2,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| k20_filter_2(sK1076,X1,X2) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X1),k7_filter_2(sK1076,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(sF1079)) ) ),
introduced(definition,[new_symbols(definition,[spl1084_498])],[avatar_definition]) ).
fof(f22729,plain,
( ! [X2,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(sF1079))
| v1_xboole_0(X1)
| v1_xboole_0(X2)
| k20_filter_2(sK1076,X1,X2) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X1),k7_filter_2(sK1076,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079)) )
| ~ spl1084_498 ),
inference(avatar_component_clause,[],[f22728]) ).
fof(f22730,plain,
( spl1084_496
| spl1084_496
| spl1084_498 ),
inference(avatar_split_clause,[],[f22719,f22728,f22721,f22721]) ).
fof(f22743,plain,
( v1_xboole_0(sK1078)
| ~ spl1084_345
| ~ spl1084_496 ),
inference(resolution,[],[f22722,f18108]) ).
fof(f22750,plain,
( $false
| ~ spl1084_345
| ~ spl1084_496 ),
inference(forward_subsumption_resolution,[],[f22743,f18668]) ).
fof(f22751,plain,
( ~ spl1084_345
| ~ spl1084_496 ),
inference(avatar_contradiction_clause,[],[f22750]) ).
fof(f22773,plain,
( ! [X0] :
( v1_xboole_0(X0)
| v1_xboole_0(sK1078)
| k20_filter_2(sK1076,X0,sK1078) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X0),k7_filter_2(sK1076,sK1078))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079)) )
| ~ spl1084_345
| ~ spl1084_498 ),
inference(resolution,[],[f22729,f18108]) ).
fof(f22779,plain,
( ! [X0] :
( v1_xboole_0(X0)
| k20_filter_2(sK1076,X0,sK1078) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X0),k7_filter_2(sK1076,sK1078))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079)) )
| ~ spl1084_345
| ~ spl1084_498 ),
inference(forward_subsumption_resolution,[],[f22773,f18668]) ).
fof(f22785,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k20_filter_2(sK1076,X0,sK1078) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,X0),sK1078) )
| ~ spl1084_345
| ~ spl1084_498 ),
inference(forward_demodulation,[],[f22779,f19463]) ).
fof(f22839,plain,
( v1_xboole_0(sK1077)
| k20_filter_2(sK1076,sK1077,sK1078) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,sK1077),sK1078)
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_498 ),
inference(resolution,[],[f22785,f18112]) ).
fof(f22847,plain,
( k20_filter_2(sK1076,sK1077,sK1078) = k5_filter_0(k1_lattice2(sK1076),k7_filter_2(sK1076,sK1077),sK1078)
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_498 ),
inference(forward_subsumption_resolution,[],[f22839,f18669]) ).
fof(f22853,plain,
( k20_filter_2(sK1076,sK1077,sK1078) = k5_filter_0(k1_lattice2(sK1076),sK1077,sK1078)
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_498 ),
inference(forward_demodulation,[],[f22847,f19658]) ).
fof(f22857,plain,
( sF1082 = k5_filter_0(k1_lattice2(sK1076),sK1077,sK1078)
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_498 ),
inference(forward_demodulation,[],[f22853,f15459]) ).
fof(f22863,plain,
( k3_filter_0(k1_lattice2(sK1076),sF1080) = k3_filter_0(k1_lattice2(sK1076),sF1082)
| ~ spl1084_345
| ~ spl1084_346
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| ~ spl1084_498 ),
inference(superposition,[],[f20475,f22857]) ).
fof(f23257,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ v1_xboole_0(k20_filter_2(sK1076,X1,X0)) ),
inference(superposition,[],[f13502,f15453]) ).
fof(f23264,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ v1_xboole_0(k20_filter_2(sK1076,X1,X0)) ),
inference(forward_subsumption_resolution,[],[f23257,f13523]) ).
fof(f23268,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| ~ l3_lattices(sK1076)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ v1_xboole_0(k20_filter_2(sK1076,X1,X0)) ),
inference(forward_subsumption_resolution,[],[f23264,f13522]) ).
fof(f23270,plain,
! [X0,X1] :
( ~ v1_xboole_0(k20_filter_2(sK1076,X1,X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079)) ),
inference(forward_subsumption_resolution,[],[f23268,f13521]) ).
fof(f23271,plain,
( ~ v1_xboole_0(sF1082)
| v1_xboole_0(sK1077)
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079)) ),
inference(superposition,[],[f23270,f15459]) ).
fof(f23274,plain,
( v1_xboole_0(sK1077)
| ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| ~ spl1084_386 ),
inference(forward_subsumption_resolution,[],[f23271,f18782]) ).
fof(f23276,plain,
( ~ m1_subset_1(sK1077,k1_zfmisc_1(sF1079))
| v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| ~ spl1084_386 ),
inference(forward_subsumption_resolution,[],[f23274,f18669]) ).
fof(f23278,plain,
( v1_xboole_0(sK1078)
| ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| ~ spl1084_346
| ~ spl1084_386 ),
inference(forward_subsumption_resolution,[],[f23276,f18112]) ).
fof(f23280,plain,
( ~ m1_subset_1(sK1078,k1_zfmisc_1(sF1079))
| ~ spl1084_346
| ~ spl1084_386 ),
inference(forward_subsumption_resolution,[],[f23278,f18668]) ).
fof(f23283,plain,
( $false
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_386 ),
inference(forward_subsumption_resolution,[],[f23280,f18108]) ).
fof(f23284,plain,
( ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_386 ),
inference(avatar_contradiction_clause,[],[f23283]) ).
fof(f23323,plain,
( k3_filter_0(k1_lattice2(sK1076),sF1082) = k3_filter_2(k1_lattice2(sK1076),sF1082)
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_386
| ~ spl1084_389 ),
inference(forward_subsumption_resolution,[],[f22558,f18781]) ).
fof(f23367,plain,
( k3_filter_0(k1_lattice2(sK1076),sF1080) = k3_filter_2(k1_lattice2(sK1076),sF1082)
| ~ spl1084_345
| ~ spl1084_346
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_386
| ~ spl1084_389
| ~ spl1084_498 ),
inference(forward_demodulation,[],[f23323,f22863]) ).
fof(f26116,plain,
( k4_subset_1(sF1079,sK1077,sK1078) = k4_subset_1(sF1079,sK1078,sK1077)
| ~ spl1084_345
| ~ spl1084_346 ),
inference(resolution,[],[f19359,f18112]) ).
fof(f26127,plain,
( k4_subset_1(sF1079,sK1077,sK1078) = k3_tarski(k2_tarski(sK1078,sK1077))
| ~ spl1084_345
| ~ spl1084_346 ),
inference(forward_demodulation,[],[f26116,f20871]) ).
fof(f26139,plain,
( sF1080 = k3_tarski(k2_tarski(sK1078,sK1077))
| ~ spl1084_345
| ~ spl1084_346 ),
inference(forward_demodulation,[],[f26127,f15455]) ).
fof(f26145,plain,
( sF1080 = k4_subset_1(sF1079,sF1080,sK1077)
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_403 ),
inference(superposition,[],[f20879,f26139]) ).
fof(f26150,plain,
( sF1080 = k3_tarski(k2_tarski(sF1080,sK1077))
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_347
| ~ spl1084_403 ),
inference(forward_demodulation,[],[f26145,f20873]) ).
fof(f26193,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k19_filter_2(sK1076,X1) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076)))
| v3_struct_0(sK1076)
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(superposition,[],[f13481,f18092]) ).
fof(f26196,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k19_filter_2(sK1076,X1) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076)))
| ~ v10_lattices(sK1076)
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f26193,f13523]) ).
fof(f26200,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k19_filter_2(sK1076,X1) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076)))
| ~ l3_lattices(sK1076) ),
inference(forward_subsumption_resolution,[],[f26196,f13522]) ).
fof(f26204,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k19_filter_2(sK1076,X1) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1076))) ),
inference(forward_subsumption_resolution,[],[f26200,f13521]) ).
fof(f26207,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF1079))
| v1_xboole_0(X0)
| k19_filter_2(sK1076,X1) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,X1))
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f26204,f15453]) ).
fof(f26213,definition,
( spl1084_618
<=> ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X1)
| k19_filter_2(sK1076,X1) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl1084_618])],[avatar_definition]) ).
fof(f26214,plain,
( ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF1079))
| v1_xboole_0(X1)
| k19_filter_2(sK1076,X1) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,X1)) )
| ~ spl1084_618 ),
inference(avatar_component_clause,[],[f26213]) ).
fof(f26215,plain,
( spl1084_496
| spl1084_618 ),
inference(avatar_split_clause,[],[f26207,f26213,f22721]) ).
fof(f26234,plain,
( v1_xboole_0(sF1080)
| k19_filter_2(sK1076,sF1080) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,sF1080))
| ~ spl1084_347
| ~ spl1084_618 ),
inference(resolution,[],[f26214,f18117]) ).
fof(f26235,plain,
( v1_xboole_0(sF1082)
| k19_filter_2(sK1076,sF1082) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,sF1082))
| ~ spl1084_389
| ~ spl1084_618 ),
inference(resolution,[],[f26214,f18793]) ).
fof(f26239,plain,
( k19_filter_2(sK1076,sF1082) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,sF1082))
| spl1084_386
| ~ spl1084_389
| ~ spl1084_618 ),
inference(forward_subsumption_resolution,[],[f26235,f18781]) ).
fof(f26249,plain,
( k19_filter_2(sK1076,sF1082) = k3_filter_2(k1_lattice2(sK1076),sF1082)
| spl1084_386
| ~ spl1084_389
| ~ spl1084_618 ),
inference(forward_demodulation,[],[f26239,f19833]) ).
fof(f26257,plain,
( k19_filter_2(sK1076,sF1082) = k3_filter_0(k1_lattice2(sK1076),sF1080)
| ~ spl1084_345
| ~ spl1084_346
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_386
| ~ spl1084_389
| ~ spl1084_498
| ~ spl1084_618 ),
inference(forward_demodulation,[],[f26249,f23367]) ).
fof(f26265,plain,
( sF1083 = k3_filter_0(k1_lattice2(sK1076),sF1080)
| ~ spl1084_345
| ~ spl1084_346
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_386
| ~ spl1084_389
| ~ spl1084_498
| ~ spl1084_618 ),
inference(forward_demodulation,[],[f26257,f15461]) ).
fof(f55594,definition,
( spl1084_1118
<=> sF1081 = sF1083 ),
introduced(definition,[new_symbols(definition,[spl1084_1118])],[avatar_definition]) ).
fof(f55596,plain,
( sF1081 = sF1083
| ~ spl1084_1118 ),
inference(avatar_component_clause,[],[f55594]) ).
fof(f55625,definition,
( spl1084_1125
<=> r1_tarski(sF1080,sK1077) ),
introduced(definition,[new_symbols(definition,[spl1084_1125])],[avatar_definition]) ).
fof(f55626,plain,
( r1_tarski(sF1080,sK1077)
| ~ spl1084_1125 ),
inference(avatar_component_clause,[],[f55625]) ).
fof(f55627,plain,
( ~ r1_tarski(sF1080,sK1077)
| spl1084_1125 ),
inference(avatar_component_clause,[],[f55625]) ).
fof(f55727,plain,
( ~ v1_xboole_0(sF1080)
| spl1084_1125 ),
inference(resolution,[],[f55627,f21786]) ).
fof(f55728,plain,
( $false
| ~ spl1084_390
| spl1084_1125 ),
inference(forward_subsumption_resolution,[],[f55727,f18799]) ).
fof(f55729,plain,
( ~ spl1084_390
| spl1084_1125 ),
inference(avatar_contradiction_clause,[],[f55728]) ).
fof(f55765,plain,
( sK1077 = k3_tarski(k2_tarski(sF1080,sK1077))
| ~ spl1084_1125 ),
inference(resolution,[],[f55626,f17317]) ).
fof(f55771,plain,
( sK1077 = sF1080
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_347
| ~ spl1084_403
| ~ spl1084_1125 ),
inference(forward_demodulation,[],[f55765,f26150]) ).
fof(f56196,definition,
( spl1084_1132
<=> sK1077 = sF1080 ),
introduced(definition,[new_symbols(definition,[spl1084_1132])],[avatar_definition]) ).
fof(f56198,plain,
( sK1077 = sF1080
| ~ spl1084_1132 ),
inference(avatar_component_clause,[],[f56196]) ).
fof(f56204,plain,
( spl1084_1132
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_347
| ~ spl1084_403
| ~ spl1084_1125 ),
inference(avatar_split_clause,[],[f55771,f55625,f18862,f18115,f18111,f18107,f56196]) ).
fof(f56470,plain,
( ~ v1_xboole_0(sF1080)
| ~ spl1084_1132 ),
inference(superposition,[],[f18669,f56198]) ).
fof(f56816,plain,
( $false
| ~ spl1084_390
| ~ spl1084_1132 ),
inference(forward_subsumption_resolution,[],[f56470,f18799]) ).
fof(f56817,plain,
( ~ spl1084_390
| ~ spl1084_1132 ),
inference(avatar_contradiction_clause,[],[f56816]) ).
fof(f56891,plain,
( k3_filter_0(k1_lattice2(sK1076),sF1080) = k3_filter_2(k1_lattice2(sK1076),sF1080)
| ~ spl1084_347
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_390 ),
inference(forward_subsumption_resolution,[],[f22557,f18798]) ).
fof(f56907,plain,
( k19_filter_2(sK1076,sF1080) = k3_filter_2(k1_lattice2(sK1076),k7_filter_2(sK1076,sF1080))
| ~ spl1084_347
| spl1084_390
| ~ spl1084_618 ),
inference(forward_subsumption_resolution,[],[f26234,f18798]) ).
fof(f57037,plain,
( k19_filter_2(sK1076,sF1080) = k3_filter_2(k1_lattice2(sK1076),sF1080)
| ~ spl1084_347
| spl1084_390
| ~ spl1084_618 ),
inference(forward_demodulation,[],[f56907,f19928]) ).
fof(f57442,plain,
( sF1083 = k3_filter_2(k1_lattice2(sK1076),sF1080)
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_347
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_386
| ~ spl1084_389
| spl1084_390
| ~ spl1084_498
| ~ spl1084_618 ),
inference(forward_demodulation,[],[f56891,f26265]) ).
fof(f57456,plain,
( sF1081 = k3_filter_2(k1_lattice2(sK1076),sF1080)
| ~ spl1084_347
| spl1084_390
| ~ spl1084_618 ),
inference(forward_demodulation,[],[f57037,f15457]) ).
fof(f58429,plain,
( sF1081 = sF1083
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_347
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_386
| ~ spl1084_389
| spl1084_390
| ~ spl1084_498
| ~ spl1084_618 ),
inference(forward_demodulation,[],[f57442,f57456]) ).
fof(f58477,plain,
( spl1084_1118
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_347
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_386
| ~ spl1084_389
| spl1084_390
| ~ spl1084_498
| ~ spl1084_618 ),
inference(avatar_split_clause,[],[f58429,f26213,f22728,f18797,f18792,f18780,f18408,f18404,f18173,f18115,f18111,f18107,f55594]) ).
fof(f58486,plain,
( ~ r1_filter_2(sF1079,sF1081,sF1081)
| ~ spl1084_1118 ),
inference(superposition,[],[f15462,f55596]) ).
fof(f58808,plain,
( $false
| ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_1118 ),
inference(forward_subsumption_resolution,[],[f58486,f19827]) ).
fof(f58809,plain,
( ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_1118 ),
inference(avatar_contradiction_clause,[],[f58808]) ).
cnf(s297,plain,
( ~ spl1084_345
| ~ spl1084_346
| spl1084_347 ),
inference(sat_conversion,[],[f18118]) ).
cnf(s314,plain,
( spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_370 ),
inference(sat_conversion,[],[f18486]) ).
cnf(s358,plain,
spl1084_345,
inference(sat_conversion,[],[f19040]) ).
cnf(s365,plain,
spl1084_356,
inference(sat_conversion,[],[f19310]) ).
cnf(s367,plain,
spl1084_357,
inference(sat_conversion,[],[f19324]) ).
cnf(s368,plain,
~ spl1084_349,
inference(sat_conversion,[],[f19366]) ).
cnf(s373,plain,
( spl1084_346
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| ~ spl1084_370 ),
inference(sat_conversion,[],[f19755]) ).
cnf(s376,plain,
( ~ spl1084_345
| ~ spl1084_346
| spl1084_403 ),
inference(sat_conversion,[],[f19788]) ).
cnf(s378,plain,
( ~ spl1084_345
| ~ spl1084_346
| spl1084_389 ),
inference(sat_conversion,[],[f19818]) ).
cnf(s431,plain,
( spl1084_496
| spl1084_496
| spl1084_498 ),
inference(sat_conversion,[],[f22730]) ).
cnf(s432,plain,
( spl1084_496
| spl1084_498 ),
inference(rat,[],[s431]) ).
cnf(s434,plain,
( ~ spl1084_345
| ~ spl1084_496 ),
inference(sat_conversion,[],[f22751]) ).
cnf(s439,plain,
( ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_386 ),
inference(sat_conversion,[],[f23284]) ).
cnf(s592,plain,
( spl1084_496
| spl1084_618 ),
inference(sat_conversion,[],[f26215]) ).
cnf(s1218,plain,
( ~ spl1084_390
| spl1084_1125 ),
inference(sat_conversion,[],[f55729]) ).
cnf(s1230,plain,
( ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_347
| ~ spl1084_403
| ~ spl1084_1125
| spl1084_1132 ),
inference(sat_conversion,[],[f56204]) ).
cnf(s1251,plain,
( ~ spl1084_390
| ~ spl1084_1132 ),
inference(sat_conversion,[],[f56817]) ).
cnf(s1304,plain,
( ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_347
| spl1084_349
| ~ spl1084_356
| ~ spl1084_357
| spl1084_386
| ~ spl1084_389
| spl1084_390
| ~ spl1084_498
| ~ spl1084_618
| spl1084_1118 ),
inference(sat_conversion,[],[f58477]) ).
cnf(s1310,plain,
( ~ spl1084_345
| ~ spl1084_346
| ~ spl1084_1118 ),
inference(sat_conversion,[],[f58809]) ).
cnf(s1354,plain,
~ spl1084_496,
inference(rat,[],[s434,s358]) ).
cnf(s1365,plain,
spl1084_618,
inference(rat,[],[s592,s1354]) ).
cnf(s1366,plain,
spl1084_498,
inference(rat,[],[s432,s1354]) ).
cnf(s1394,plain,
spl1084_370,
inference(rat,[],[s314,s367,s365,s368]) ).
cnf(s1396,plain,
spl1084_346,
inference(rat,[],[s373,s365,s367,s368,s1394]) ).
cnf(s1411,plain,
~ spl1084_1118,
inference(rat,[],[s1310,s358,s1396]) ).
cnf(s1426,plain,
~ spl1084_386,
inference(rat,[],[s439,s358,s1396]) ).
cnf(s1431,plain,
spl1084_389,
inference(rat,[],[s378,s358,s1396]) ).
cnf(s1432,plain,
spl1084_403,
inference(rat,[],[s376,s358,s1396]) ).
cnf(s1527,plain,
spl1084_347,
inference(rat,[],[s297,s1396,s358]) ).
cnf(s1528,plain,
spl1084_390,
inference(rat,[],[s1304,s1411,s1365,s1366,s1426,s1431,s1396,s367,s365,s368,s358,s1527]) ).
cnf(s1529,plain,
~ spl1084_1132,
inference(rat,[],[s1251,s1528]) ).
cnf(s1530,plain,
spl1084_1125,
inference(rat,[],[s1218,s1528]) ).
cnf(s1533,plain,
$false,
inference(rat,[],[s1230,s1527,s1432,s1396,s358,s1529,s1530]) ).
fof(f58861,plain,
$false,
inference(avatar_sat_refutation,[],[s1533]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT318+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n003.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 14:35:57 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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
% 11.36/2.36 % (600721)Detected formulas, will run a generic FOF schedule.
% 11.36/2.36 % (600731)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3506159929:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.36/2.36 % (600730)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3592977054:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.36/2.36 % (600732)dis-21_1_sil=8000:lcm=predicate:random_seed=1268841800:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.36/2.36 % (600727)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=1614453514:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.36/2.36 % (600728)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=4175692927:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.36/2.36 % (600729)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1712872298:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.36/2.36 % (600726)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=3684903492:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.36/2.36 % (600731)Instruction limit reached!
% 11.36/2.36 % (600731)------------------------------
% 11.36/2.36 % (600731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.36/2.36 % (600731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.36/2.36 % (600731)CaDiCaL version: 2.1.3
% 11.36/2.36 % (600731)Termination reason: Instruction limit
% 11.36/2.36 % (600731)Termination phase: Clausification
% 11.36/2.36 % (600731)Time elapsed: 0.049 s
% 11.36/2.36 % (600731)Peak memory usage: 94 MB
% 11.36/2.36 % (600731)Instructions burned: 139 (million)
% 11.36/2.36 % (600729)Refutation not found, incomplete strategy
% 11.36/2.36 % (600729)------------------------------
% 11.36/2.36 % (600729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.36/2.36 % (600729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.36/2.36 % (600729)CaDiCaL version: 2.1.3
% 11.36/2.36 % (600729)Termination reason: Refutation not found, incomplete strategy
% 11.36/2.36 % (600729)Time elapsed: 0.015 s
% 11.36/2.36 % (600729)Peak memory usage: 91 MB
% 11.36/2.36 % (600729)Instructions burned: 19 (million)
% 11.36/2.36 % (600732)Instruction limit reached!
% 11.36/2.36 % (600732)------------------------------
% 11.36/2.36 % (600732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.36/2.36 % (600732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.36/2.36 % (600732)CaDiCaL version: 2.1.3
% 11.36/2.36 % (600732)Termination reason: Instruction limit
% 11.36/2.36 % (600732)Termination phase: Property scanning
% 11.36/2.36 % (600732)Time elapsed: 0.079 s
% 11.36/2.36 % (600732)Peak memory usage: 92 MB
% 11.36/2.36 % (600732)Instructions burned: 130 (million)
% 11.36/2.36 % (600730)Instruction limit reached!
% 11.36/2.36 % (600730)------------------------------
% 11.36/2.36 % (600730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.36/2.36 % (600730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.36/2.36 % (600730)CaDiCaL version: 2.1.3
% 11.36/2.36 % (600730)Termination reason: Instruction limit
% 11.36/2.36 % (600730)Termination phase: Saturation
% 11.36/2.36 % (600730)Time elapsed: 0.079 s
% 11.36/2.36 % (600730)Peak memory usage: 92 MB
% 11.36/2.36 % (600730)Instructions burned: 120 (million)
% 11.36/2.36 % (600740)lrs+10_1_sil=8000:sp=occurrence:random_seed=3584132779:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.36/2.36 % (600740)Instruction limit reached!
% 11.36/2.36 % (600740)------------------------------
% 11.36/2.36 % (600740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.36/2.36 % (600740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.36/2.36 % (600740)CaDiCaL version: 2.1.3
% 11.36/2.36 % (600740)Termination reason: Instruction limit
% 11.36/2.36 % (600740)Termination phase: Saturation
% 11.36/2.36 % (600740)Time elapsed: 0.107 s
% 11.36/2.36 % (600740)Peak memory usage: 95 MB
% 11.36/2.36 % (600740)Instructions burned: 288 (million)
% 11.36/2.36 % (600741)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3765164528:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 17.95/3.24 % (600742)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1188749297:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 17.95/3.24 % (600741)Refutation not found, incomplete strategy
% 17.95/3.24 % (600741)------------------------------
% 17.95/3.24 % (600741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.95/3.24 % (600741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.95/3.24 % (600741)CaDiCaL version: 2.1.3
% 17.95/3.24 % (600741)Termination reason: Refutation not found, incomplete strategy
% 17.95/3.24 % (600741)Time elapsed: 0.034 s
% 17.95/3.24 % (600741)Peak memory usage: 92 MB
% 17.95/3.24 % (600741)Instructions burned: 60 (million)
% 17.95/3.24 % (600742)Refutation not found, incomplete strategy
% 17.95/3.24 % (600742)------------------------------
% 17.95/3.24 % (600742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.95/3.24 % (600742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.95/3.24 % (600742)CaDiCaL version: 2.1.3
% 17.95/3.24 % (600742)Termination reason: Refutation not found, incomplete strategy
% 17.95/3.24 % (600742)Time elapsed: 0.024 s
% 17.95/3.24 % (600742)Peak memory usage: 92 MB
% 17.95/3.24 % (600742)Instructions burned: 34 (million)
% 17.95/3.24 % (600729)------------------------------
% 17.95/3.24 % (600729)------------------------------
% 17.95/3.24 % (600745)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=2326335132:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 17.95/3.24 % (600745)Instruction limit reached!
% 17.95/3.24 % (600745)------------------------------
% 17.95/3.24 % (600745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.95/3.24 % (600745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.95/3.24 % (600745)CaDiCaL version: 2.1.3
% 17.95/3.24 % (600745)Termination reason: Instruction limit
% 17.95/3.24 % (600745)Termination phase: Saturation
% 17.95/3.24 % (600745)Time elapsed: 0.077 s
% 17.95/3.24 % (600745)Peak memory usage: 98 MB
% 17.95/3.24 % (600745)Instructions burned: 249 (million)
% 17.95/3.24 % (600747)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=824636121:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 17.95/3.24 % (600749)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=214499345:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 17.95/3.24 % (600742)------------------------------
% 17.95/3.24 % (600742)------------------------------
% 17.95/3.24 % (600741)------------------------------
% 17.95/3.24 % (600741)------------------------------
% 17.95/3.24 % (600747)Instruction limit reached!
% 17.95/3.24 % (600747)------------------------------
% 17.95/3.24 % (600747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.95/3.24 % (600747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.95/3.24 % (600747)CaDiCaL version: 2.1.3
% 17.95/3.24 % (600747)Termination reason: Instruction limit
% 17.95/3.24 % (600747)Termination phase: Saturation
% 17.95/3.24 % (600747)Time elapsed: 0.179 s
% 17.95/3.24 % (600747)Peak memory usage: 95 MB
% 17.95/3.24 % (600747)Instructions burned: 295 (million)
% 17.95/3.24 % (600753)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=699100959:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 17.95/3.24 % (600752)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=715812142:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 17.95/3.24 % (600752)Instruction limit reached!
% 17.95/3.24 % (600752)------------------------------
% 17.95/3.24 % (600752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.95/3.24 % (600752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.95/3.24 % (600752)CaDiCaL version: 2.1.3
% 17.95/3.24 % (600752)Termination reason: Instruction limit
% 17.95/3.24 % (600752)Termination phase: Saturation
% 17.95/3.24 % (600752)Time elapsed: 0.063 s
% 17.95/3.24 % (600752)Peak memory usage: 93 MB
% 17.95/3.24 % (600752)Instructions burned: 113 (million)
% 17.95/3.24 % (600753)Instruction limit reached!
% 17.95/3.24 % (600753)------------------------------
% 17.95/3.24 % (600753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.95/3.24 % (600753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600753)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600753)Termination reason: Instruction limit
% 40.83/6.45 % (600753)Termination phase: Property scanning
% 40.83/6.45 % (600753)Time elapsed: 0.078 s
% 40.83/6.45 % (600753)Peak memory usage: 94 MB
% 40.83/6.45 % (600753)Instructions burned: 128 (million)
% 40.83/6.45 % (600754)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2008621976:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 40.83/6.45 % (600754)Instruction limit reached!
% 40.83/6.45 % (600754)------------------------------
% 40.83/6.45 % (600754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600754)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600754)Termination reason: Instruction limit
% 40.83/6.45 % (600754)Termination phase: Property scanning
% 40.83/6.45 % (600754)Time elapsed: 0.061 s
% 40.83/6.45 % (600754)Peak memory usage: 91 MB
% 40.83/6.45 % (600754)Instructions burned: 116 (million)
% 40.83/6.45 % (600757)lrs+10_1_sil=8000:sp=occurrence:random_seed=877691071:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 40.83/6.45 % (600758)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=228233810:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 40.83/6.45 % (600760)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4092830134:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 40.83/6.45 % (600758)Instruction limit reached!
% 40.83/6.45 % (600758)------------------------------
% 40.83/6.45 % (600758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600758)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600758)Termination reason: Instruction limit
% 40.83/6.45 % (600758)Termination phase: Saturation
% 40.83/6.45 % (600758)Time elapsed: 0.245 s
% 40.83/6.45 % (600758)Peak memory usage: 95 MB
% 40.83/6.45 % (600758)Instructions burned: 437 (million)
% 40.83/6.45 % (600764)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3526926344:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 40.83/6.45 % (600749)Instruction limit reached!
% 40.83/6.45 % (600749)------------------------------
% 40.83/6.45 % (600749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600749)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600749)Termination reason: Instruction limit
% 40.83/6.45 % (600749)Termination phase: Saturation
% 40.83/6.45 % (600749)Time elapsed: 0.833 s
% 40.83/6.45 % (600749)Peak memory usage: 219 MB
% 40.83/6.45 % (600749)Instructions burned: 2353 (million)
% 40.83/6.45 % (600764)Instruction limit reached!
% 40.83/6.45 % (600764)------------------------------
% 40.83/6.45 % (600764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600764)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600764)Termination reason: Instruction limit
% 40.83/6.45 % (600764)Termination phase: Saturation
% 40.83/6.45 % (600764)Time elapsed: 0.081 s
% 40.83/6.45 % (600764)Peak memory usage: 94 MB
% 40.83/6.45 % (600764)Instructions burned: 135 (million)
% 40.83/6.45 % (600767)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4030546262:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 40.83/6.45 % (600757)Instruction limit reached!
% 40.83/6.45 % (600757)------------------------------
% 40.83/6.45 % (600757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600757)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600757)Termination reason: Instruction limit
% 40.83/6.45 % (600757)Termination phase: Saturation
% 40.83/6.45 % (600757)Time elapsed: 0.597 s
% 40.83/6.45 % (600757)Peak memory usage: 103 MB
% 40.83/6.45 % (600757)Instructions burned: 909 (million)
% 40.83/6.45 % (600766)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1158484269:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 40.83/6.45 % (600770)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=651440686:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 40.83/6.45 % (600770)Instruction limit reached!
% 40.83/6.45 % (600770)------------------------------
% 40.83/6.45 % (600770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600770)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600770)Termination reason: Instruction limit
% 40.83/6.45 % (600770)Termination phase: Saturation
% 40.83/6.45 % (600770)Time elapsed: 0.071 s
% 40.83/6.45 % (600770)Peak memory usage: 93 MB
% 40.83/6.45 % (600770)Instructions burned: 126 (million)
% 40.83/6.45 % (600766)Instruction limit reached!
% 40.83/6.45 % (600766)------------------------------
% 40.83/6.45 % (600766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600766)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600766)Termination reason: Instruction limit
% 40.83/6.45 % (600766)Termination phase: Saturation
% 40.83/6.45 % (600766)Time elapsed: 0.298 s
% 40.83/6.45 % (600766)Peak memory usage: 102 MB
% 40.83/6.45 % (600766)Instructions burned: 593 (million)
% 40.83/6.45 % (600772)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3509365423:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 40.83/6.45 % (600772)Instruction limit reached!
% 40.83/6.45 % (600772)------------------------------
% 40.83/6.45 % (600772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600772)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600772)Termination reason: Instruction limit
% 40.83/6.45 % (600772)Termination phase: Preprocessing 3
% 40.83/6.45 % (600772)Time elapsed: 0.077 s
% 40.83/6.45 % (600772)Peak memory usage: 92 MB
% 40.83/6.45 % (600772)Instructions burned: 135 (million)
% 40.83/6.45 % (600773)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2985058700:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 40.83/6.45 % (600773)Instruction limit reached!
% 40.83/6.45 % (600773)------------------------------
% 40.83/6.45 % (600773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600773)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600773)Termination reason: Instruction limit
% 40.83/6.45 % (600773)Termination phase: Saturation
% 40.83/6.45 % (600773)Time elapsed: 0.078 s
% 40.83/6.45 % (600773)Peak memory usage: 93 MB
% 40.83/6.45 % (600773)Instructions burned: 143 (million)
% 40.83/6.45 % (600775)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2163623513:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 40.83/6.45 % (600775)Refutation not found, incomplete strategy
% 40.83/6.45 % (600775)------------------------------
% 40.83/6.45 % (600775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600775)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600775)Termination reason: Refutation not found, incomplete strategy
% 40.83/6.45 % (600775)Time elapsed: 0.019 s
% 40.83/6.45 % (600775)Peak memory usage: 92 MB
% 40.83/6.45 % (600775)Instructions burned: 25 (million)
% 40.83/6.45 % (600777)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=215129268:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 40.83/6.45 % (600775)------------------------------
% 40.83/6.45 % (600775)------------------------------
% 40.83/6.45 % (600780)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=1950134247:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi)
% 40.83/6.45 % (600780)Instruction limit reached!
% 40.83/6.45 % (600780)------------------------------
% 40.83/6.45 % (600780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600780)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600780)Termination reason: Instruction limit
% 40.83/6.45 % (600780)Termination phase: Property scanning
% 40.83/6.45 % (600780)Time elapsed: 0.084 s
% 40.83/6.45 % (600780)Peak memory usage: 94 MB
% 40.83/6.45 % (600780)Instructions burned: 151 (million)
% 40.83/6.45 % (600782)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4044704572:i=14155:bd=all_2973 on theBenchmark for (2973ds/14155Mi)
% 40.83/6.45 % (600760)Instruction limit reached!
% 40.83/6.45 % (600760)------------------------------
% 40.83/6.45 % (600760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600760)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600760)Termination reason: Instruction limit
% 40.83/6.45 % (600760)Termination phase: Saturation
% 40.83/6.45 % (600760)Time elapsed: 3.114 s
% 40.83/6.45 % (600760)Peak memory usage: 188 MB
% 40.83/6.45 % (600760)Instructions burned: 5202 (million)
% 40.83/6.45 % (600784)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1652086757:i=667:av=off:fsr=off_2957 on theBenchmark for (2957ds/667Mi)
% 40.83/6.45 % (600784)Instruction limit reached!
% 40.83/6.45 % (600784)------------------------------
% 40.83/6.45 % (600784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600784)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600784)Termination reason: Instruction limit
% 40.83/6.45 % (600784)Termination phase: Saturation
% 40.83/6.45 % (600784)Time elapsed: 0.288 s
% 40.83/6.45 % (600784)Peak memory usage: 101 MB
% 40.83/6.45 % (600784)Instructions burned: 669 (million)
% 40.83/6.45 % (600786)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3558187397:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 40.83/6.45 % (600786)Instruction limit reached!
% 40.83/6.45 % (600786)------------------------------
% 40.83/6.45 % (600786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600786)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600786)Termination reason: Instruction limit
% 40.83/6.45 % (600786)Termination phase: Property scanning
% 40.83/6.45 % (600786)Time elapsed: 0.106 s
% 40.83/6.45 % (600786)Peak memory usage: 94 MB
% 40.83/6.45 % (600786)Instructions burned: 186 (million)
% 40.83/6.45 % (600788)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2837733413:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 40.83/6.45 % (600788)Instruction limit reached!
% 40.83/6.45 % (600788)------------------------------
% 40.83/6.45 % (600788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.83/6.45 % (600788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.83/6.45 % (600788)CaDiCaL version: 2.1.3
% 40.83/6.45 % (600788)Termination reason: Instruction limit
% 40.83/6.45 % (600788)Termination phase: Saturation
% 40.83/6.45 % (600788)Time elapsed: 0.117 s
% 40.83/6.45 % (600788)Peak memory usage: 95 MB
% 40.83/6.45 % (600788)Instructions burned: 194 (million)
% 40.83/6.45 % (600790)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=548130533:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2948 on theBenchmark for (2948ds/4850Mi)
% 40.83/6.45 % (600726)First to succeed.
% 40.83/6.45 % (600726)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-600721"
% 40.83/6.45 % (600726)Refutation found. Thanks to Tanya!
% 40.83/6.45 % SZS status Theorem for theBenchmark
% 40.83/6.45 % SZS output start Proof for theBenchmark
% See solution above
% 41.35/6.65 % (600726)------------------------------
% 41.35/6.65 % (600726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.35/6.65 % (600726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.35/6.65 % (600726)CaDiCaL version: 2.1.3
% 41.35/6.65 % (600726)Termination reason: Refutation
% 41.35/6.65 % (600726)Time elapsed: 5.350 s
% 41.35/6.65 % (600726)Peak memory usage: 221 MB
% 41.35/6.65 % (600726)Instructions burned: 8690 (million)
% 41.35/6.65 % (600726)------------------------------
% 41.35/6.65 % (600726)------------------------------
% 41.35/6.65 % (600721)Success in time 5.83 s
% 41.35/6.65 % Vampire exiting
%------------------------------------------------------------------------------