%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT315+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 : n010.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:50 AM UTC 2026
% Result : Theorem 70.64s 11.01s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 67
% Syntax : Number of formulae : 607 ( 81 unt; 38 def)
% Number of atoms : 2291 ( 246 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 2813 (1129 ~;1425 |; 177 &)
% ( 38 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 28 prp; 0-3 aty)
% Number of functors : 33 ( 33 usr; 13 con; 0-3 aty)
% Number of variables : 423 ( 0 sgn 412 !; 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(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(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(f514,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ( r1_tarski(X1,X2)
<=> r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_subset_1) ).
fof(f524,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> r1_tarski(k3_subset_1(X0,k4_subset_1(X0,X1,X2)),k3_subset_1(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_subset_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(f2455,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f2493,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))) )
=> ( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
& k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,k3_filter_0(X0,X2))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t47_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(f2544,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m1_filter_0(k3_filter_0(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_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] :
( 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(f2877,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f2883,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(f2908,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m2_filter_2(k19_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k19_filter_2) ).
fof(f2942,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f2964,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( m2_filter_2(X3,X0)
=> ( r1_tarski(X1,X3)
=> r1_tarski(X2,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_filter_2) ).
fof(f2966,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_filter_2) ).
fof(f2967,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t38_filter_2) ).
fof(f2982,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( 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(f2983,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( 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)))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2982]) ).
fof(f3075,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f3098,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f3307,plain,
! [X0,X1] :
( ! [X2] :
( ( r1_tarski(X1,X2)
<=> r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f514]) ).
fof(f3319,plain,
! [X0,X1] :
( ! [X2] :
( r1_tarski(k3_subset_1(X0,k4_subset_1(X0,X1,X2)),k3_subset_1(X0,X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f524]) ).
fof(f3383,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(f3384,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,[],[f3383]) ).
fof(f3385,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(f3386,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,[],[f3385]) ).
fof(f3389,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(f3390,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,[],[f3389]) ).
fof(f5479,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2455]) ).
fof(f5480,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5479]) ).
fof(f5537,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
& k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,k3_filter_0(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,[],[f2493]) ).
fof(f5538,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
& k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,k3_filter_0(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,[],[f5537]) ).
fof(f5623,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(f5624,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,[],[f5623]) ).
fof(f5631,plain,
! [X0,X1] :
( m1_filter_0(k3_filter_0(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f2544]) ).
fof(f5632,plain,
! [X0,X1] :
( m1_filter_0(k3_filter_0(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f5631]) ).
fof(f5671,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(f5672,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5671]) ).
fof(f5681,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(f5682,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,[],[f5681]) ).
fof(f5722,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(f5723,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,[],[f5722]) ).
fof(f5858,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f6037,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(f6038,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,[],[f6037]) ).
fof(f6069,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2873]) ).
fof(f6070,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,[],[f6069]) ).
fof(f6077,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f2877]) ).
fof(f6078,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f6077]) ).
fof(f6089,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,[],[f2883]) ).
fof(f6090,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,[],[f6089]) ).
fof(f6139,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f2908]) ).
fof(f6140,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f6139]) ).
fof(f6204,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2942]) ).
fof(f6205,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,[],[f6204]) ).
fof(f6248,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2964]) ).
fof(f6249,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,[],[f6248]) ).
fof(f6252,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2966]) ).
fof(f6253,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,[],[f6252]) ).
fof(f6254,plain,
! [X0] :
( ! [X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2967]) ).
fof(f6255,plain,
! [X0] :
( ! [X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6254]) ).
fof(f6284,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(f6285,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,[],[f6284]) ).
fof(f6460,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(f6461,plain,
! [X0] :
( sP112(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f5682,f6460]) ).
fof(f6492,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,[],[f3075]) ).
fof(f6493,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,[],[f6492]) ).
fof(f6494,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))],[f6493]) ).
fof(f6530,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(f6531,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,[],[f6530]) ).
fof(f6656,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r1_tarski(X1,X2)
| ~ r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1)) )
& ( r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1))
| ~ r1_tarski(X1,X2) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f3307]) ).
fof(f7862,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,[],[f6460]) ).
fof(f7987,plain,
! [X0,X1,X2] :
( ( ( r1_filter_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_filter_2(X0,X1,X2) ) )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f6078]) ).
fof(f8022,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,[],[f6249]) ).
fof(f8023,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,[],[f8022]) ).
fof(f8024,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,[],[f8023]) ).
fof(f8025,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK1069(X0,X1,X2))
& r1_tarski(X1,sK1069(X0,X1,X2))
& m2_filter_2(sK1069(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,[sK1069]),skolemize(X3,sK1069(X0,X1,X2))],[f8024]) ).
fof(f8032,plain,
( ( ~ r1_filter_2(u1_struct_0(sK1074),k19_filter_2(sK1074,k4_subset_1(u1_struct_0(sK1074),sK1075,sK1076)),k19_filter_2(sK1074,k4_subset_1(u1_struct_0(sK1074),k19_filter_2(sK1074,sK1075),sK1076)))
| ~ r1_filter_2(u1_struct_0(sK1074),k19_filter_2(sK1074,k4_subset_1(u1_struct_0(sK1074),sK1075,sK1076)),k19_filter_2(sK1074,k4_subset_1(u1_struct_0(sK1074),sK1075,k19_filter_2(sK1074,sK1076)))) )
& ~ v1_xboole_0(sK1076)
& m1_subset_1(sK1076,k1_zfmisc_1(u1_struct_0(sK1074)))
& ~ v1_xboole_0(sK1075)
& m1_subset_1(sK1075,k1_zfmisc_1(u1_struct_0(sK1074)))
& ~ v3_struct_0(sK1074)
& v10_lattices(sK1074)
& l3_lattices(sK1074) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1074,sK1075,sK1076]),skolemize(X0,sK1074),skolemize(X1,sK1075),skolemize(X2,sK1076)],[f6285]) ).
fof(f8047,plain,
! [X0,X1] :
( r2_hidden(sK127(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f6494]) ).
fof(f8113,plain,
! [X0,X1] :
( r1_tarski(X1,X0)
| X0 != X1 ),
inference(cnf_transformation,[],[f6531]) ).
fof(f8115,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f6531]) ).
fof(f8160,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f3098]) ).
fof(f8214,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f8264,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(f8578,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k3_tarski(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f418]) ).
fof(f8723,plain,
! [X2,X0,X1] :
( ~ r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1))
| r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f6656]) ).
fof(f8734,plain,
! [X2,X0,X1] :
( r1_tarski(k3_subset_1(X0,k4_subset_1(X0,X1,X2)),k3_subset_1(X0,X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f3319]) ).
fof(f8803,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,[],[f3384]) ).
fof(f8804,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,[],[f3386]) ).
fof(f8806,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,[],[f3390]) ).
fof(f12514,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5480]) ).
fof(f12585,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X2)
| k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,k3_filter_0(X0,X2)))
| 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,[],[f5538]) ).
fof(f12586,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X2)
| k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k3_filter_0(X0,k4_subset_1(u1_struct_0(X0),k3_filter_0(X0,X1),X2))
| 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,[],[f5538]) ).
fof(f12679,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,[],[f5624]) ).
fof(f12680,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5624]) ).
fof(f12684,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)
| m1_filter_0(k3_filter_0(X0,X1),X0) ),
inference(cnf_transformation,[],[f5632]) ).
fof(f12728,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5672]) ).
fof(f12749,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP112(X0) ),
inference(cnf_transformation,[],[f7862]) ).
fof(f12758,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP112(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6461]) ).
fof(f12875,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5723]) ).
fof(f12996,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5858]) ).
fof(f13258,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,[],[f6038]) ).
fof(f13287,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,[],[f6070]) ).
fof(f13288,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,[],[f6070]) ).
fof(f13293,plain,
! [X2,X0,X1] :
( r1_filter_2(X0,X1,X2)
| X1 != X2
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f7987]) ).
fof(f13299,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,[],[f6090]) ).
fof(f13326,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)
| m2_filter_2(k19_filter_2(X0,X1),X0) ),
inference(cnf_transformation,[],[f6140]) ).
fof(f13400,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,[],[f6205]) ).
fof(f13453,plain,
! [X2,X0,X1] :
( r1_tarski(X1,sK1069(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,[],[f8025]) ).
fof(f13454,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X2,sK1069(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,[],[f8025]) ).
fof(f13460,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,[],[f6253]) ).
fof(f13461,plain,
! [X0,X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6255]) ).
fof(f13495,plain,
l3_lattices(sK1074),
inference(cnf_transformation,[],[f8032]) ).
fof(f13496,plain,
v10_lattices(sK1074),
inference(cnf_transformation,[],[f8032]) ).
fof(f13497,plain,
~ v3_struct_0(sK1074),
inference(cnf_transformation,[],[f8032]) ).
fof(f13498,plain,
m1_subset_1(sK1075,k1_zfmisc_1(u1_struct_0(sK1074))),
inference(cnf_transformation,[],[f8032]) ).
fof(f13499,plain,
~ v1_xboole_0(sK1075),
inference(cnf_transformation,[],[f8032]) ).
fof(f13500,plain,
m1_subset_1(sK1076,k1_zfmisc_1(u1_struct_0(sK1074))),
inference(cnf_transformation,[],[f8032]) ).
fof(f13501,plain,
~ v1_xboole_0(sK1076),
inference(cnf_transformation,[],[f8032]) ).
fof(f13502,plain,
( ~ r1_filter_2(u1_struct_0(sK1074),k19_filter_2(sK1074,k4_subset_1(u1_struct_0(sK1074),sK1075,sK1076)),k19_filter_2(sK1074,k4_subset_1(u1_struct_0(sK1074),k19_filter_2(sK1074,sK1075),sK1076)))
| ~ r1_filter_2(u1_struct_0(sK1074),k19_filter_2(sK1074,k4_subset_1(u1_struct_0(sK1074),sK1075,sK1076)),k19_filter_2(sK1074,k4_subset_1(u1_struct_0(sK1074),sK1075,k19_filter_2(sK1074,sK1076)))) ),
inference(cnf_transformation,[],[f8032]) ).
fof(f13503,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,[],[f8264,f8214]) ).
fof(f13817,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,[],[f8578,f13503]) ).
fof(f13897,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,[],[f8806,f13503]) ).
fof(f14872,plain,
! [X1] : r1_tarski(X1,X1),
inference(equality_resolution,[],[f8113]) ).
fof(f15391,plain,
! [X2,X0] :
( r1_filter_2(X0,X2,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(equality_resolution,[],[f13293]) ).
fof(f15427,definition,
sF1077 = u1_struct_0(sK1074),
introduced(definition,[new_symbols(definition,[sF1077])],[function_definition]) ).
fof(f15428,plain,
u1_struct_0(sK1074) = sF1077,
inference(reorient_equations,[],[f15427]) ).
fof(f15429,definition,
sF1078 = k4_subset_1(sF1077,sK1075,sK1076),
introduced(definition,[new_symbols(definition,[sF1078])],[function_definition]) ).
fof(f15430,plain,
k4_subset_1(sF1077,sK1075,sK1076) = sF1078,
inference(reorient_equations,[],[f15429]) ).
fof(f15431,definition,
sF1079 = k19_filter_2(sK1074,sF1078),
introduced(definition,[new_symbols(definition,[sF1079])],[function_definition]) ).
fof(f15432,plain,
k19_filter_2(sK1074,sF1078) = sF1079,
inference(reorient_equations,[],[f15431]) ).
fof(f15433,definition,
sF1080 = k19_filter_2(sK1074,sK1075),
introduced(definition,[new_symbols(definition,[sF1080])],[function_definition]) ).
fof(f15434,plain,
k19_filter_2(sK1074,sK1075) = sF1080,
inference(reorient_equations,[],[f15433]) ).
fof(f15435,definition,
sF1081 = k4_subset_1(sF1077,sF1080,sK1076),
introduced(definition,[new_symbols(definition,[sF1081])],[function_definition]) ).
fof(f15436,plain,
k4_subset_1(sF1077,sF1080,sK1076) = sF1081,
inference(reorient_equations,[],[f15435]) ).
fof(f15437,definition,
sF1082 = k19_filter_2(sK1074,sF1081),
introduced(definition,[new_symbols(definition,[sF1082])],[function_definition]) ).
fof(f15438,plain,
k19_filter_2(sK1074,sF1081) = sF1082,
inference(reorient_equations,[],[f15437]) ).
fof(f15439,definition,
sF1083 = k19_filter_2(sK1074,sK1076),
introduced(definition,[new_symbols(definition,[sF1083])],[function_definition]) ).
fof(f15440,plain,
k19_filter_2(sK1074,sK1076) = sF1083,
inference(reorient_equations,[],[f15439]) ).
fof(f15441,definition,
sF1084 = k4_subset_1(sF1077,sK1075,sF1083),
introduced(definition,[new_symbols(definition,[sF1084])],[function_definition]) ).
fof(f15442,plain,
k4_subset_1(sF1077,sK1075,sF1083) = sF1084,
inference(reorient_equations,[],[f15441]) ).
fof(f15443,definition,
sF1085 = k19_filter_2(sK1074,sF1084),
introduced(definition,[new_symbols(definition,[sF1085])],[function_definition]) ).
fof(f15444,plain,
k19_filter_2(sK1074,sF1084) = sF1085,
inference(reorient_equations,[],[f15443]) ).
fof(f15445,plain,
( ~ r1_filter_2(sF1077,sF1079,sF1082)
| ~ r1_filter_2(sF1077,sF1079,sF1085) ),
inference(definition_folding,[],[f13502,f15444,f15442,f15440,f15428,f15432,f15430,f15428,f15428,f15438,f15436,f15434,f15428,f15432,f15430,f15428,f15428]) ).
fof(f15446,definition,
sF1086 = k1_zfmisc_1(sF1077),
introduced(definition,[new_symbols(definition,[sF1086])],[function_definition]) ).
fof(f15447,plain,
k1_zfmisc_1(sF1077) = sF1086,
inference(reorient_equations,[],[f15446]) ).
fof(f15448,plain,
m1_subset_1(sK1076,sF1086),
inference(definition_folding,[],[f13500,f15447,f15428]) ).
fof(f15449,plain,
m1_subset_1(sK1075,sF1086),
inference(definition_folding,[],[f13498,f15447,f15428]) ).
fof(f15453,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| r1_filter_2(X0,X2,X2) ),
inference(duplicate_literal_removal,[],[f15391]) ).
fof(f15509,definition,
( spl1087_1
<=> r1_filter_2(sF1077,sF1079,sF1085) ),
introduced(definition,[new_symbols(definition,[spl1087_1])],[avatar_definition]) ).
fof(f15511,plain,
( ~ r1_filter_2(sF1077,sF1079,sF1085)
| spl1087_1 ),
inference(avatar_component_clause,[],[f15509]) ).
fof(f15513,definition,
( spl1087_2
<=> r1_filter_2(sF1077,sF1079,sF1082) ),
introduced(definition,[new_symbols(definition,[spl1087_2])],[avatar_definition]) ).
fof(f15515,plain,
( ~ r1_filter_2(sF1077,sF1079,sF1082)
| spl1087_2 ),
inference(avatar_component_clause,[],[f15513]) ).
fof(f15516,plain,
( ~ spl1087_1
| ~ spl1087_2 ),
inference(avatar_split_clause,[],[f15445,f15513,f15509]) ).
fof(f18072,plain,
( m1_subset_1(sF1084,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077)) ),
inference(superposition,[],[f8803,f15442]) ).
fof(f18073,plain,
( m1_subset_1(sF1084,sF1086)
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077)) ),
inference(forward_demodulation,[],[f18072,f15447]) ).
fof(f18074,plain,
( ~ m1_subset_1(sK1075,sF1086)
| m1_subset_1(sF1084,sF1086)
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077)) ),
inference(forward_demodulation,[],[f18073,f15447]) ).
fof(f18075,plain,
( m1_subset_1(sF1084,sF1086)
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077)) ),
inference(forward_subsumption_resolution,[],[f18074,f15449]) ).
fof(f18076,plain,
( ~ m1_subset_1(sF1083,sF1086)
| m1_subset_1(sF1084,sF1086) ),
inference(forward_demodulation,[],[f18075,f15447]) ).
fof(f18078,definition,
( spl1087_353
<=> m1_subset_1(sF1084,sF1086) ),
introduced(definition,[new_symbols(definition,[spl1087_353])],[avatar_definition]) ).
fof(f18080,plain,
( m1_subset_1(sF1084,sF1086)
| ~ spl1087_353 ),
inference(avatar_component_clause,[],[f18078]) ).
fof(f18082,definition,
( spl1087_354
<=> m1_subset_1(sF1083,sF1086) ),
introduced(definition,[new_symbols(definition,[spl1087_354])],[avatar_definition]) ).
fof(f18083,plain,
( m1_subset_1(sF1083,sF1086)
| ~ spl1087_354 ),
inference(avatar_component_clause,[],[f18082]) ).
fof(f18084,plain,
( ~ m1_subset_1(sF1083,sF1086)
| spl1087_354 ),
inference(avatar_component_clause,[],[f18082]) ).
fof(f18085,plain,
( spl1087_353
| ~ spl1087_354 ),
inference(avatar_split_clause,[],[f18076,f18082,f18078]) ).
fof(f18086,plain,
( m1_subset_1(sF1081,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sF1080,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077)) ),
inference(superposition,[],[f8803,f15436]) ).
fof(f18087,plain,
( m1_subset_1(sF1081,sF1086)
| ~ m1_subset_1(sF1080,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077)) ),
inference(forward_demodulation,[],[f18086,f15447]) ).
fof(f18088,plain,
( ~ m1_subset_1(sF1080,sF1086)
| m1_subset_1(sF1081,sF1086)
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077)) ),
inference(forward_demodulation,[],[f18087,f15447]) ).
fof(f18089,plain,
( ~ m1_subset_1(sK1076,sF1086)
| ~ m1_subset_1(sF1080,sF1086)
| m1_subset_1(sF1081,sF1086) ),
inference(forward_demodulation,[],[f18088,f15447]) ).
fof(f18090,plain,
( ~ m1_subset_1(sF1080,sF1086)
| m1_subset_1(sF1081,sF1086) ),
inference(forward_subsumption_resolution,[],[f18089,f15448]) ).
fof(f18092,definition,
( spl1087_355
<=> m1_subset_1(sF1081,sF1086) ),
introduced(definition,[new_symbols(definition,[spl1087_355])],[avatar_definition]) ).
fof(f18094,plain,
( m1_subset_1(sF1081,sF1086)
| ~ spl1087_355 ),
inference(avatar_component_clause,[],[f18092]) ).
fof(f18096,definition,
( spl1087_356
<=> m1_subset_1(sF1080,sF1086) ),
introduced(definition,[new_symbols(definition,[spl1087_356])],[avatar_definition]) ).
fof(f18097,plain,
( m1_subset_1(sF1080,sF1086)
| ~ spl1087_356 ),
inference(avatar_component_clause,[],[f18096]) ).
fof(f18098,plain,
( ~ m1_subset_1(sF1080,sF1086)
| spl1087_356 ),
inference(avatar_component_clause,[],[f18096]) ).
fof(f18099,plain,
( spl1087_355
| ~ spl1087_356 ),
inference(avatar_split_clause,[],[f18090,f18096,f18092]) ).
fof(f18100,plain,
( m1_subset_1(sF1078,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077)) ),
inference(superposition,[],[f8803,f15430]) ).
fof(f18101,plain,
( m1_subset_1(sF1078,sF1086)
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077)) ),
inference(forward_demodulation,[],[f18100,f15447]) ).
fof(f18102,plain,
( ~ m1_subset_1(sK1075,sF1086)
| m1_subset_1(sF1078,sF1086)
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077)) ),
inference(forward_demodulation,[],[f18101,f15447]) ).
fof(f18103,plain,
( m1_subset_1(sF1078,sF1086)
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077)) ),
inference(forward_subsumption_resolution,[],[f18102,f15449]) ).
fof(f18104,plain,
( ~ m1_subset_1(sK1076,sF1086)
| m1_subset_1(sF1078,sF1086) ),
inference(forward_demodulation,[],[f18103,f15447]) ).
fof(f18105,plain,
m1_subset_1(sF1078,sF1086),
inference(forward_subsumption_resolution,[],[f18104,f15448]) ).
fof(f18106,plain,
! [X0] :
( r1_filter_2(sF1077,k19_filter_2(sK1074,X0),X0)
| ~ m2_filter_2(X0,sK1074)
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(superposition,[],[f13461,f15428]) ).
fof(f18107,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK1074,X0),sK1074) ),
inference(superposition,[],[f13326,f15428]) ).
fof(f18108,plain,
! [X0] :
( r1_filter_2(sF1077,k19_filter_2(sK1074,X0),X0)
| ~ m2_filter_2(X0,sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18106,f13497]) ).
fof(f18109,plain,
! [X0] :
( r1_filter_2(sF1077,k19_filter_2(sK1074,X0),X0)
| ~ m2_filter_2(X0,sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18108,f13496]) ).
fof(f18110,plain,
! [X0] :
( r1_filter_2(sF1077,k19_filter_2(sK1074,X0),X0)
| ~ m2_filter_2(X0,sK1074) ),
inference(forward_subsumption_resolution,[],[f18109,f13495]) ).
fof(f18114,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1086)
| ~ m1_subset_1(X0,sF1086)
| k4_subset_1(sF1077,X0,X1) = k4_subset_1(sF1077,X1,X0) ),
inference(superposition,[],[f8804,f15447]) ).
fof(f18115,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1086)
| k4_subset_1(sF1077,X0,sK1076) = k4_subset_1(sF1077,sK1076,X0) ),
inference(resolution,[],[f18114,f15448]) ).
fof(f18116,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1086)
| k4_subset_1(sF1077,X0,sK1075) = k4_subset_1(sF1077,sK1075,X0) ),
inference(resolution,[],[f18114,f15449]) ).
fof(f18118,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF1086)
| ~ m1_subset_1(X1,sF1086)
| k5_xboole_0(k5_xboole_0(X1,X0),k4_xboole_0(X1,k4_xboole_0(X1,X0))) = k4_subset_1(sF1077,X1,X0) ),
inference(superposition,[],[f13897,f15447]) ).
fof(f18119,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1086)
| ~ m1_subset_1(X0,sF1086)
| k3_tarski(k2_tarski(X1,X0)) = k4_subset_1(sF1077,X1,X0) ),
inference(forward_demodulation,[],[f18118,f13817]) ).
fof(f18128,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1086)
| k4_subset_1(sF1077,sK1076,X0) = k3_tarski(k2_tarski(sK1076,X0)) ),
inference(resolution,[],[f18119,f15448]) ).
fof(f18153,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,[],[f13453,f13454]) ).
fof(f18154,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,[],[f18153]) ).
fof(f18155,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,[],[f18154,f13288]) ).
fof(f18156,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,[],[f18155,f14872]) ).
fof(f18164,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| k7_filter_2(sK1074,X0) = X0
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(superposition,[],[f13400,f15428]) ).
fof(f18165,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| k7_filter_2(sK1074,X0) = X0
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18164,f13497]) ).
fof(f18166,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| k7_filter_2(sK1074,X0) = X0
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18165,f13496]) ).
fof(f18167,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| k7_filter_2(sK1074,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f18166,f13495]) ).
fof(f18168,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1086)
| k7_filter_2(sK1074,X0) = X0 ),
inference(forward_demodulation,[],[f18167,f15447]) ).
fof(f18169,plain,
sK1076 = k7_filter_2(sK1074,sK1076),
inference(resolution,[],[f18168,f15448]) ).
fof(f18170,plain,
sK1075 = k7_filter_2(sK1074,sK1075),
inference(resolution,[],[f18168,f15449]) ).
fof(f18171,plain,
sF1078 = k7_filter_2(sK1074,sF1078),
inference(resolution,[],[f18168,f18105]) ).
fof(f18200,plain,
! [X0,X1] :
( r1_filter_2(u1_struct_0(X1),X0,X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v1_xboole_0(u1_struct_0(X1))
| ~ m1_filter_0(X0,X1) ),
inference(resolution,[],[f12679,f15453]) ).
fof(f18215,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| k7_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f13258,f13400]) ).
fof(f18216,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f13258,f18156]) ).
fof(f18222,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ m2_lattice4(X0,sK1074)
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(superposition,[],[f13258,f15428]) ).
fof(f18224,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0 ),
inference(duplicate_literal_removal,[],[f18216]) ).
fof(f18225,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| k7_filter_2(X1,X0) = X0 ),
inference(duplicate_literal_removal,[],[f18215]) ).
fof(f18226,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ m2_lattice4(X0,sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18222,f13497]) ).
fof(f18228,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| k19_filter_2(X1,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f18224,f13287]) ).
fof(f18229,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ m2_lattice4(X0,sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18226,f13496]) ).
fof(f18230,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ m2_lattice4(X0,sK1074) ),
inference(forward_subsumption_resolution,[],[f18229,f13495]) ).
fof(f18231,plain,
! [X0] :
( ~ m2_lattice4(X0,sK1074)
| m1_subset_1(X0,sF1086) ),
inference(forward_demodulation,[],[f18230,f15447]) ).
fof(f18274,definition,
( spl1087_359
<=> m1_filter_0(sF1077,sK1074) ),
introduced(definition,[new_symbols(definition,[spl1087_359])],[avatar_definition]) ).
fof(f18275,plain,
( m1_filter_0(sF1077,sK1074)
| ~ spl1087_359 ),
inference(avatar_component_clause,[],[f18274]) ).
fof(f18284,plain,
( v3_struct_0(sK1074)
| u1_struct_0(sK1074) = u1_struct_0(k1_lattice2(sK1074)) ),
inference(resolution,[],[f12875,f13495]) ).
fof(f18285,plain,
u1_struct_0(sK1074) = u1_struct_0(k1_lattice2(sK1074)),
inference(forward_subsumption_resolution,[],[f18284,f13497]) ).
fof(f18286,plain,
sF1077 = u1_struct_0(k1_lattice2(sK1074)),
inference(forward_demodulation,[],[f18285,f15428]) ).
fof(f18287,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1074)))
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(superposition,[],[f13460,f18286]) ).
fof(f18288,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,k3_filter_0(k1_lattice2(sK1074),X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077))
| v3_struct_0(k1_lattice2(sK1074))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074)) ),
inference(superposition,[],[f12585,f18286]) ).
fof(f18289,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,k3_filter_0(k1_lattice2(sK1074),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077))
| v3_struct_0(k1_lattice2(sK1074))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074)) ),
inference(superposition,[],[f12586,f18286]) ).
fof(f18292,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v3_struct_0(k1_lattice2(sK1074))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),X0) = k3_filter_2(k1_lattice2(sK1074),X0) ),
inference(superposition,[],[f13299,f18286]) ).
fof(f18301,definition,
( spl1087_360
<=> l3_lattices(k1_lattice2(sK1074)) ),
introduced(definition,[new_symbols(definition,[spl1087_360])],[avatar_definition]) ).
fof(f18302,plain,
( l3_lattices(k1_lattice2(sK1074))
| ~ spl1087_360 ),
inference(avatar_component_clause,[],[f18301]) ).
fof(f18303,plain,
( ~ l3_lattices(k1_lattice2(sK1074))
| spl1087_360 ),
inference(avatar_component_clause,[],[f18301]) ).
fof(f18305,definition,
( spl1087_361
<=> v10_lattices(k1_lattice2(sK1074)) ),
introduced(definition,[new_symbols(definition,[spl1087_361])],[avatar_definition]) ).
fof(f18306,plain,
( v10_lattices(k1_lattice2(sK1074))
| ~ spl1087_361 ),
inference(avatar_component_clause,[],[f18305]) ).
fof(f18307,plain,
( ~ v10_lattices(k1_lattice2(sK1074))
| spl1087_361 ),
inference(avatar_component_clause,[],[f18305]) ).
fof(f18309,definition,
( spl1087_362
<=> v3_struct_0(k1_lattice2(sK1074)) ),
introduced(definition,[new_symbols(definition,[spl1087_362])],[avatar_definition]) ).
fof(f18310,plain,
( ~ v3_struct_0(k1_lattice2(sK1074))
| spl1087_362 ),
inference(avatar_component_clause,[],[f18309]) ).
fof(f18311,plain,
( v3_struct_0(k1_lattice2(sK1074))
| ~ spl1087_362 ),
inference(avatar_component_clause,[],[f18309]) ).
fof(f18337,plain,
( m1_filter_0(sF1077,sK1074)
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(superposition,[],[f12514,f15428]) ).
fof(f18339,plain,
( m1_filter_0(sF1077,sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18337,f13497]) ).
fof(f18341,plain,
( m1_filter_0(sF1077,sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18339,f13496]) ).
fof(f18343,plain,
m1_filter_0(sF1077,sK1074),
inference(forward_subsumption_resolution,[],[f18341,f13495]) ).
fof(f18345,plain,
spl1087_359,
inference(avatar_split_clause,[],[f18343,f18274]) ).
fof(f18370,definition,
( spl1087_368
<=> m2_filter_2(sF1079,sK1074) ),
introduced(definition,[new_symbols(definition,[spl1087_368])],[avatar_definition]) ).
fof(f18371,plain,
( m2_filter_2(sF1079,sK1074)
| ~ spl1087_368 ),
inference(avatar_component_clause,[],[f18370]) ).
fof(f18372,plain,
( ~ m2_filter_2(sF1079,sK1074)
| spl1087_368 ),
inference(avatar_component_clause,[],[f18370]) ).
fof(f18474,plain,
( r1_tarski(k3_subset_1(sF1077,sF1078),k3_subset_1(sF1077,sK1075))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077)) ),
inference(superposition,[],[f8734,f15430]) ).
fof(f18481,plain,
( ~ m1_subset_1(sK1076,sF1086)
| r1_tarski(k3_subset_1(sF1077,sF1078),k3_subset_1(sF1077,sK1075))
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077)) ),
inference(forward_demodulation,[],[f18474,f15447]) ).
fof(f18485,plain,
( r1_tarski(k3_subset_1(sF1077,sF1078),k3_subset_1(sF1077,sK1075))
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077)) ),
inference(forward_subsumption_resolution,[],[f18481,f15448]) ).
fof(f18488,plain,
( ~ m1_subset_1(sK1075,sF1086)
| r1_tarski(k3_subset_1(sF1077,sF1078),k3_subset_1(sF1077,sK1075)) ),
inference(forward_demodulation,[],[f18485,f15447]) ).
fof(f18490,plain,
r1_tarski(k3_subset_1(sF1077,sF1078),k3_subset_1(sF1077,sK1075)),
inference(forward_subsumption_resolution,[],[f18488,f15449]) ).
fof(f18503,plain,
( ~ l3_lattices(sK1074)
| spl1087_360 ),
inference(resolution,[],[f12996,f18303]) ).
fof(f18505,plain,
( $false
| spl1087_360 ),
inference(forward_subsumption_resolution,[],[f18503,f13495]) ).
fof(f18506,plain,
spl1087_360,
inference(avatar_contradiction_clause,[],[f18505]) ).
fof(f18514,plain,
( v3_struct_0(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_362 ),
inference(resolution,[],[f18311,f12728]) ).
fof(f18515,plain,
( ~ l3_lattices(sK1074)
| ~ spl1087_362 ),
inference(forward_subsumption_resolution,[],[f18514,f13497]) ).
fof(f18516,plain,
( $false
| ~ spl1087_362 ),
inference(forward_subsumption_resolution,[],[f18515,f13495]) ).
fof(f18517,plain,
~ spl1087_362,
inference(avatar_contradiction_clause,[],[f18516]) ).
fof(f18525,plain,
( ~ v1_xboole_0(sF1077)
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_359 ),
inference(resolution,[],[f12680,f18275]) ).
fof(f18537,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK1074,X0),sK1074) ),
inference(forward_subsumption_resolution,[],[f18107,f13497]) ).
fof(f18539,definition,
( spl1087_375
<=> v1_xboole_0(sF1077) ),
introduced(definition,[new_symbols(definition,[spl1087_375])],[avatar_definition]) ).
fof(f18540,plain,
( ~ v1_xboole_0(sF1077)
| spl1087_375 ),
inference(avatar_component_clause,[],[f18539]) ).
fof(f18569,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1074)))
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18287,f13497]) ).
fof(f18582,plain,
( ~ v1_xboole_0(sF1077)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_359 ),
inference(forward_subsumption_resolution,[],[f18525,f13497]) ).
fof(f18587,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK1074,X0),sK1074) ),
inference(forward_subsumption_resolution,[],[f18537,f13496]) ).
fof(f18607,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1074)))
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f18569,f13496]) ).
fof(f18623,plain,
( ~ v1_xboole_0(sF1077)
| ~ l3_lattices(sK1074)
| ~ spl1087_359 ),
inference(forward_subsumption_resolution,[],[f18582,f13496]) ).
fof(f18628,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK1074,X0),sK1074) ),
inference(forward_subsumption_resolution,[],[f18587,f13495]) ).
fof(f18648,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1074))) ),
inference(forward_subsumption_resolution,[],[f18607,f13495]) ).
fof(f18665,plain,
( ~ v1_xboole_0(sF1077)
| ~ spl1087_359 ),
inference(forward_subsumption_resolution,[],[f18623,f13495]) ).
fof(f18670,plain,
! [X0] :
( m2_filter_2(k19_filter_2(sK1074,X0),sK1074)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(forward_demodulation,[],[f18628,f15447]) ).
fof(f18685,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1074))) ),
inference(forward_demodulation,[],[f18648,f15447]) ).
fof(f18694,plain,
( ~ spl1087_375
| ~ spl1087_359 ),
inference(avatar_split_clause,[],[f18665,f18274,f18539]) ).
fof(f18711,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1))
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f18685,f15428]) ).
fof(f18721,definition,
( spl1087_381
<=> v1_xboole_0(sF1081) ),
introduced(definition,[new_symbols(definition,[spl1087_381])],[avatar_definition]) ).
fof(f18722,plain,
( ~ v1_xboole_0(sF1081)
| spl1087_381 ),
inference(avatar_component_clause,[],[f18721]) ).
fof(f18723,plain,
( v1_xboole_0(sF1081)
| ~ spl1087_381 ),
inference(avatar_component_clause,[],[f18721]) ).
fof(f18730,definition,
( spl1087_383
<=> v1_xboole_0(sF1084) ),
introduced(definition,[new_symbols(definition,[spl1087_383])],[avatar_definition]) ).
fof(f18731,plain,
( ~ v1_xboole_0(sF1084)
| spl1087_383 ),
inference(avatar_component_clause,[],[f18730]) ).
fof(f18732,plain,
( v1_xboole_0(sF1084)
| ~ spl1087_383 ),
inference(avatar_component_clause,[],[f18730]) ).
fof(f18759,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1086)
| ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1))
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f18711,f15447]) ).
fof(f18777,definition,
( spl1087_388
<=> ! [X0] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl1087_388])],[avatar_definition]) ).
fof(f18778,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0) )
| ~ spl1087_388 ),
inference(avatar_component_clause,[],[f18777]) ).
fof(f18780,definition,
( spl1087_389
<=> ! [X1] :
( ~ m1_subset_1(X1,sF1086)
| v1_xboole_0(X1)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl1087_389])],[avatar_definition]) ).
fof(f18781,plain,
( ! [X1] :
( ~ m1_subset_1(X1,sF1086)
| v1_xboole_0(X1)
| k19_filter_2(sK1074,X1) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,X1)) )
| ~ spl1087_389 ),
inference(avatar_component_clause,[],[f18780]) ).
fof(f18782,plain,
( spl1087_388
| spl1087_389 ),
inference(avatar_split_clause,[],[f18759,f18780,f18777]) ).
fof(f18795,definition,
( spl1087_391
<=> m2_filter_2(sF1080,sK1074) ),
introduced(definition,[new_symbols(definition,[spl1087_391])],[avatar_definition]) ).
fof(f18796,plain,
( m2_filter_2(sF1080,sK1074)
| ~ spl1087_391 ),
inference(avatar_component_clause,[],[f18795]) ).
fof(f18797,plain,
( ~ m2_filter_2(sF1080,sK1074)
| spl1087_391 ),
inference(avatar_component_clause,[],[f18795]) ).
fof(f18804,definition,
( spl1087_393
<=> m2_filter_2(sF1083,sK1074) ),
introduced(definition,[new_symbols(definition,[spl1087_393])],[avatar_definition]) ).
fof(f18805,plain,
( m2_filter_2(sF1083,sK1074)
| ~ spl1087_393 ),
inference(avatar_component_clause,[],[f18804]) ).
fof(f18806,plain,
( ~ m2_filter_2(sF1083,sK1074)
| spl1087_393 ),
inference(avatar_component_clause,[],[f18804]) ).
fof(f18847,definition,
( spl1087_400
<=> v1_xboole_0(sF1078) ),
introduced(definition,[new_symbols(definition,[spl1087_400])],[avatar_definition]) ).
fof(f18848,plain,
( ~ v1_xboole_0(sF1078)
| spl1087_400 ),
inference(avatar_component_clause,[],[f18847]) ).
fof(f18849,plain,
( v1_xboole_0(sF1078)
| ~ spl1087_400 ),
inference(avatar_component_clause,[],[f18847]) ).
fof(f18861,plain,
( v1_xboole_0(sK1075)
| ~ spl1087_388 ),
inference(resolution,[],[f18778,f15449]) ).
fof(f18869,plain,
( $false
| ~ spl1087_388 ),
inference(forward_subsumption_resolution,[],[f18861,f13499]) ).
fof(f18870,plain,
~ spl1087_388,
inference(avatar_contradiction_clause,[],[f18869]) ).
fof(f18872,plain,
( v1_xboole_0(sK1075)
| k19_filter_2(sK1074,sK1075) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sK1075))
| ~ spl1087_389 ),
inference(resolution,[],[f18781,f15449]) ).
fof(f18873,plain,
( v1_xboole_0(sK1076)
| k19_filter_2(sK1074,sK1076) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sK1076))
| ~ spl1087_389 ),
inference(resolution,[],[f18781,f15448]) ).
fof(f18875,plain,
( v1_xboole_0(sF1078)
| k19_filter_2(sK1074,sF1078) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sF1078))
| ~ spl1087_389 ),
inference(resolution,[],[f18781,f18105]) ).
fof(f18877,plain,
( k19_filter_2(sK1074,sK1076) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sK1076))
| ~ spl1087_389 ),
inference(forward_subsumption_resolution,[],[f18873,f13501]) ).
fof(f18878,plain,
( k19_filter_2(sK1074,sK1075) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sK1075))
| ~ spl1087_389 ),
inference(forward_subsumption_resolution,[],[f18872,f13499]) ).
fof(f18880,plain,
( k19_filter_2(sK1074,sK1076) = k3_filter_2(k1_lattice2(sK1074),sK1076)
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f18877,f18169]) ).
fof(f18881,plain,
( k19_filter_2(sK1074,sK1075) = k3_filter_2(k1_lattice2(sK1074),sK1075)
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f18878,f18170]) ).
fof(f18883,plain,
( sF1083 = k3_filter_2(k1_lattice2(sK1074),sK1076)
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f18880,f15440]) ).
fof(f18884,plain,
( sF1080 = k3_filter_2(k1_lattice2(sK1074),sK1075)
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f18881,f15434]) ).
fof(f18889,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| v3_struct_0(sK1074)
| k19_filter_2(sK1074,X0) = k19_filter_2(sK1074,k19_filter_2(sK1074,X0)) ),
inference(resolution,[],[f18670,f18228]) ).
fof(f18890,plain,
( m2_filter_2(sF1080,sK1074)
| v1_xboole_0(sK1075)
| ~ m1_subset_1(sK1075,sF1086) ),
inference(superposition,[],[f18670,f15434]) ).
fof(f18891,plain,
( m2_filter_2(sF1083,sK1074)
| v1_xboole_0(sK1076)
| ~ m1_subset_1(sK1076,sF1086) ),
inference(superposition,[],[f18670,f15440]) ).
fof(f18893,plain,
( m2_filter_2(sF1079,sK1074)
| v1_xboole_0(sF1078)
| ~ m1_subset_1(sF1078,sF1086) ),
inference(superposition,[],[f18670,f15432]) ).
fof(f18898,plain,
( v1_xboole_0(sK1076)
| ~ m1_subset_1(sK1076,sF1086)
| spl1087_393 ),
inference(forward_subsumption_resolution,[],[f18891,f18806]) ).
fof(f18899,plain,
( v1_xboole_0(sK1075)
| ~ m1_subset_1(sK1075,sF1086)
| spl1087_391 ),
inference(forward_subsumption_resolution,[],[f18890,f18797]) ).
fof(f18900,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086)
| ~ l3_lattices(sK1074)
| v3_struct_0(sK1074)
| k19_filter_2(sK1074,X0) = k19_filter_2(sK1074,k19_filter_2(sK1074,X0)) ),
inference(forward_subsumption_resolution,[],[f18889,f13496]) ).
fof(f18904,plain,
( ~ m1_subset_1(sK1076,sF1086)
| spl1087_393 ),
inference(forward_subsumption_resolution,[],[f18898,f13501]) ).
fof(f18905,plain,
( ~ m1_subset_1(sK1075,sF1086)
| spl1087_391 ),
inference(forward_subsumption_resolution,[],[f18899,f13499]) ).
fof(f18906,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086)
| v3_struct_0(sK1074)
| k19_filter_2(sK1074,X0) = k19_filter_2(sK1074,k19_filter_2(sK1074,X0)) ),
inference(forward_subsumption_resolution,[],[f18900,f13495]) ).
fof(f18910,plain,
( $false
| spl1087_393 ),
inference(forward_subsumption_resolution,[],[f18904,f15448]) ).
fof(f18911,plain,
spl1087_393,
inference(avatar_contradiction_clause,[],[f18910]) ).
fof(f18912,plain,
( $false
| spl1087_391 ),
inference(forward_subsumption_resolution,[],[f18905,f15449]) ).
fof(f18913,plain,
spl1087_391,
inference(avatar_contradiction_clause,[],[f18912]) ).
fof(f18914,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k19_filter_2(sK1074,X0) = k19_filter_2(sK1074,k19_filter_2(sK1074,X0)) ),
inference(forward_subsumption_resolution,[],[f18906,f13497]) ).
fof(f19630,plain,
! [X0] :
( ~ v1_xboole_0(k19_filter_2(sK1074,X0))
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(resolution,[],[f13288,f18670]) ).
fof(f19634,plain,
( ~ v1_xboole_0(sF1083)
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_393 ),
inference(resolution,[],[f13288,f18805]) ).
fof(f19637,plain,
( ~ v1_xboole_0(sF1083)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_393 ),
inference(forward_subsumption_resolution,[],[f19634,f13497]) ).
fof(f19639,plain,
! [X0] :
( ~ v1_xboole_0(k19_filter_2(sK1074,X0))
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(forward_subsumption_resolution,[],[f19630,f13497]) ).
fof(f19640,plain,
( ~ v1_xboole_0(sF1083)
| ~ l3_lattices(sK1074)
| ~ spl1087_393 ),
inference(forward_subsumption_resolution,[],[f19637,f13496]) ).
fof(f19642,plain,
! [X0] :
( ~ v1_xboole_0(k19_filter_2(sK1074,X0))
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(forward_subsumption_resolution,[],[f19639,f13496]) ).
fof(f19643,plain,
( ~ v1_xboole_0(sF1083)
| ~ spl1087_393 ),
inference(forward_subsumption_resolution,[],[f19640,f13495]) ).
fof(f19645,plain,
! [X0] :
( ~ v1_xboole_0(k19_filter_2(sK1074,X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(forward_subsumption_resolution,[],[f19642,f13495]) ).
fof(f20077,plain,
( v1_xboole_0(sF1078)
| k19_filter_2(sK1074,sF1078) = k19_filter_2(sK1074,k19_filter_2(sK1074,sF1078)) ),
inference(resolution,[],[f18914,f18105]) ).
fof(f20084,plain,
( v3_struct_0(sK1074)
| sP112(sK1074)
| ~ l3_lattices(sK1074) ),
inference(resolution,[],[f12758,f13496]) ).
fof(f20085,plain,
( sP112(sK1074)
| ~ l3_lattices(sK1074) ),
inference(forward_subsumption_resolution,[],[f20084,f13497]) ).
fof(f20086,plain,
sP112(sK1074),
inference(forward_subsumption_resolution,[],[f20085,f13495]) ).
fof(f20448,definition,
( spl1087_442
<=> m1_subset_1(sF1079,sF1086) ),
introduced(definition,[new_symbols(definition,[spl1087_442])],[avatar_definition]) ).
fof(f20449,plain,
( m1_subset_1(sF1079,sF1086)
| ~ spl1087_442 ),
inference(avatar_component_clause,[],[f20448]) ).
fof(f20450,plain,
( ~ m1_subset_1(sF1079,sF1086)
| spl1087_442 ),
inference(avatar_component_clause,[],[f20448]) ).
fof(f20512,plain,
! [X0] :
( m2_lattice4(k19_filter_2(sK1074,X0),sK1074)
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(resolution,[],[f13287,f18670]) ).
fof(f20515,plain,
( m2_lattice4(sF1080,sK1074)
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_391 ),
inference(resolution,[],[f13287,f18796]) ).
fof(f20516,plain,
( m2_lattice4(sF1083,sK1074)
| v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_393 ),
inference(resolution,[],[f13287,f18805]) ).
fof(f20519,plain,
( m2_lattice4(sF1083,sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_393 ),
inference(forward_subsumption_resolution,[],[f20516,f13497]) ).
fof(f20520,plain,
( m2_lattice4(sF1080,sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_391 ),
inference(forward_subsumption_resolution,[],[f20515,f13497]) ).
fof(f20522,plain,
! [X0] :
( m2_lattice4(k19_filter_2(sK1074,X0),sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(forward_subsumption_resolution,[],[f20512,f13497]) ).
fof(f20523,plain,
( m2_lattice4(sF1083,sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_393 ),
inference(forward_subsumption_resolution,[],[f20519,f13496]) ).
fof(f20524,plain,
( m2_lattice4(sF1080,sK1074)
| ~ l3_lattices(sK1074)
| ~ spl1087_391 ),
inference(forward_subsumption_resolution,[],[f20520,f13496]) ).
fof(f20526,plain,
! [X0] :
( m2_lattice4(k19_filter_2(sK1074,X0),sK1074)
| ~ l3_lattices(sK1074)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(forward_subsumption_resolution,[],[f20522,f13496]) ).
fof(f20527,plain,
( m2_lattice4(sF1083,sK1074)
| ~ spl1087_393 ),
inference(forward_subsumption_resolution,[],[f20523,f13495]) ).
fof(f20528,plain,
( m2_lattice4(sF1080,sK1074)
| ~ spl1087_391 ),
inference(forward_subsumption_resolution,[],[f20524,f13495]) ).
fof(f20530,plain,
! [X0] :
( m2_lattice4(k19_filter_2(sK1074,X0),sK1074)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) ),
inference(forward_subsumption_resolution,[],[f20526,f13495]) ).
fof(f20545,plain,
( m1_subset_1(sF1080,sF1086)
| ~ spl1087_391 ),
inference(resolution,[],[f20528,f18231]) ).
fof(f20550,plain,
( $false
| spl1087_356
| ~ spl1087_391 ),
inference(forward_subsumption_resolution,[],[f20545,f18098]) ).
fof(f20551,plain,
( spl1087_356
| ~ spl1087_391 ),
inference(avatar_contradiction_clause,[],[f20550]) ).
fof(f20567,plain,
( k4_subset_1(sF1077,sF1080,sK1076) = k4_subset_1(sF1077,sK1076,sF1080)
| ~ spl1087_356 ),
inference(resolution,[],[f18097,f18115]) ).
fof(f20570,plain,
( k4_subset_1(sF1077,sK1076,sF1080) = k3_tarski(k2_tarski(sK1076,sF1080))
| ~ spl1087_356 ),
inference(resolution,[],[f18097,f18128]) ).
fof(f20630,plain,
( k4_subset_1(sF1077,sF1080,sK1076) = k3_tarski(k2_tarski(sK1076,sF1080))
| ~ spl1087_356 ),
inference(forward_demodulation,[],[f20567,f20570]) ).
fof(f20641,plain,
( sF1081 = k3_tarski(k2_tarski(sK1076,sF1080))
| ~ spl1087_356 ),
inference(forward_demodulation,[],[f20630,f15436]) ).
fof(f20652,plain,
( sF1081 = k7_filter_2(sK1074,sF1081)
| ~ spl1087_355 ),
inference(resolution,[],[f18094,f18168]) ).
fof(f20658,plain,
( v1_xboole_0(sF1081)
| k19_filter_2(sK1074,sF1081) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sF1081))
| ~ spl1087_355
| ~ spl1087_389 ),
inference(resolution,[],[f18094,f18781]) ).
fof(f20711,plain,
( m1_subset_1(sF1083,sF1086)
| ~ spl1087_393 ),
inference(resolution,[],[f20527,f18231]) ).
fof(f20716,plain,
( $false
| spl1087_354
| ~ spl1087_393 ),
inference(forward_subsumption_resolution,[],[f20711,f18084]) ).
fof(f20717,plain,
( spl1087_354
| ~ spl1087_393 ),
inference(avatar_contradiction_clause,[],[f20716]) ).
fof(f20736,plain,
( k4_subset_1(sF1077,sK1075,sF1083) = k4_subset_1(sF1077,sF1083,sK1075)
| ~ spl1087_354 ),
inference(resolution,[],[f18083,f18116]) ).
fof(f20798,plain,
( sF1084 = k4_subset_1(sF1077,sF1083,sK1075)
| ~ spl1087_354 ),
inference(forward_demodulation,[],[f20736,f15442]) ).
fof(f20820,plain,
( sF1084 = k7_filter_2(sK1074,sF1084)
| ~ spl1087_353 ),
inference(resolution,[],[f18080,f18168]) ).
fof(f20826,plain,
( v1_xboole_0(sF1084)
| k19_filter_2(sK1074,sF1084) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sF1084))
| ~ spl1087_353
| ~ spl1087_389 ),
inference(resolution,[],[f18080,f18781]) ).
fof(f20853,plain,
( r1_tarski(k3_subset_1(sF1077,sF1084),k3_subset_1(sF1077,sF1083))
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077))
| ~ spl1087_354 ),
inference(superposition,[],[f8734,f20798]) ).
fof(f20856,plain,
( ~ m1_subset_1(sK1075,sF1086)
| r1_tarski(k3_subset_1(sF1077,sF1084),k3_subset_1(sF1077,sF1083))
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077))
| ~ spl1087_354 ),
inference(forward_demodulation,[],[f20853,f15447]) ).
fof(f20857,plain,
( r1_tarski(k3_subset_1(sF1077,sF1084),k3_subset_1(sF1077,sF1083))
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077))
| ~ spl1087_354 ),
inference(forward_subsumption_resolution,[],[f20856,f15449]) ).
fof(f20858,plain,
( ~ m1_subset_1(sF1083,sF1086)
| r1_tarski(k3_subset_1(sF1077,sF1084),k3_subset_1(sF1077,sF1083))
| ~ spl1087_354 ),
inference(forward_demodulation,[],[f20857,f15447]) ).
fof(f20859,plain,
( r1_tarski(k3_subset_1(sF1077,sF1084),k3_subset_1(sF1077,sF1083))
| ~ spl1087_354 ),
inference(forward_subsumption_resolution,[],[f20858,f18083]) ).
fof(f20970,plain,
! [X0] :
( m1_subset_1(k19_filter_2(sK1074,X0),sF1086)
| ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0) ),
inference(resolution,[],[f20530,f18231]) ).
fof(f20976,plain,
( m2_lattice4(sF1079,sK1074)
| v1_xboole_0(sF1078)
| ~ m1_subset_1(sF1078,sF1086) ),
inference(superposition,[],[f20530,f15432]) ).
fof(f21446,plain,
( ~ v1_xboole_0(sF1079)
| v1_xboole_0(sF1078)
| ~ m1_subset_1(sF1078,sF1086) ),
inference(superposition,[],[f19645,f15432]) ).
fof(f22842,plain,
( m1_subset_1(sF1079,sF1086)
| ~ m1_subset_1(sF1078,sF1086)
| v1_xboole_0(sF1078) ),
inference(superposition,[],[f20970,f15432]) ).
fof(f23003,plain,
! [X0] :
( r1_filter_2(sF1077,X0,X0)
| v3_struct_0(k1_lattice2(sK1074))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(sF1077)
| ~ m1_filter_0(X0,k1_lattice2(sK1074)) ),
inference(superposition,[],[f18200,f18286]) ).
fof(f23090,plain,
( ~ sP112(sK1074)
| spl1087_361 ),
inference(resolution,[],[f12749,f18307]) ).
fof(f23099,plain,
( $false
| spl1087_361 ),
inference(forward_subsumption_resolution,[],[f23090,f20086]) ).
fof(f23100,plain,
spl1087_361,
inference(avatar_contradiction_clause,[],[f23099]) ).
fof(f23109,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),X0) = k3_filter_2(k1_lattice2(sK1074),X0) )
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f18292,f18310]) ).
fof(f23110,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,k3_filter_0(k1_lattice2(sK1074),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074)) )
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f18289,f18310]) ).
fof(f23111,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,k3_filter_0(k1_lattice2(sK1074),X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074)) )
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f18288,f18310]) ).
fof(f23175,plain,
( ! [X0] :
( r1_filter_2(sF1077,X0,X0)
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(sF1077)
| ~ m1_filter_0(X0,k1_lattice2(sK1074)) )
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23003,f18310]) ).
fof(f23184,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),X0) = k3_filter_2(k1_lattice2(sK1074),X0) )
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23109,f18306]) ).
fof(f23185,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,k3_filter_0(k1_lattice2(sK1074),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077))
| ~ l3_lattices(k1_lattice2(sK1074)) )
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23110,f18306]) ).
fof(f23186,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,k3_filter_0(k1_lattice2(sK1074),X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077))
| ~ l3_lattices(k1_lattice2(sK1074)) )
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23111,f18306]) ).
fof(f23250,plain,
( ! [X0] :
( r1_filter_2(sF1077,X0,X0)
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(sF1077)
| ~ m1_filter_0(X0,k1_lattice2(sK1074)) )
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23175,f18306]) ).
fof(f23259,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),X0) = k3_filter_2(k1_lattice2(sK1074),X0) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23184,f18302]) ).
fof(f23260,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,k3_filter_0(k1_lattice2(sK1074),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077)) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23185,f18302]) ).
fof(f23261,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,k3_filter_0(k1_lattice2(sK1074),X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077)) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23186,f18302]) ).
fof(f23325,plain,
( ! [X0] :
( r1_filter_2(sF1077,X0,X0)
| v1_xboole_0(sF1077)
| ~ m1_filter_0(X0,k1_lattice2(sK1074)) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f23250,f18302]) ).
fof(f23331,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),X0) = k3_filter_2(k1_lattice2(sK1074),X0) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_demodulation,[],[f23259,f15447]) ).
fof(f23332,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,k3_filter_0(k1_lattice2(sK1074),X1),X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077)) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_demodulation,[],[f23260,f15447]) ).
fof(f23333,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,k3_filter_0(k1_lattice2(sK1074),X0)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1077)) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_demodulation,[],[f23261,f15447]) ).
fof(f23410,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK1074))
| r1_filter_2(sF1077,X0,X0) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_375 ),
inference(forward_subsumption_resolution,[],[f23325,f18540]) ).
fof(f23413,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF1086)
| ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,k3_filter_0(k1_lattice2(sK1074),X1),X0))
| v1_xboole_0(X1) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_demodulation,[],[f23332,f15447]) ).
fof(f23414,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF1086)
| ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,X1,k3_filter_0(k1_lattice2(sK1074),X0)))
| v1_xboole_0(X1) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_demodulation,[],[f23333,f15447]) ).
fof(f23732,plain,
( k19_filter_2(sK1074,sF1081) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sF1081))
| ~ spl1087_355
| spl1087_381
| ~ spl1087_389 ),
inference(forward_subsumption_resolution,[],[f20658,f18722]) ).
fof(f23787,plain,
( k19_filter_2(sK1074,sF1081) = k3_filter_2(k1_lattice2(sK1074),sF1081)
| ~ spl1087_355
| spl1087_381
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f23732,f20652]) ).
fof(f24035,plain,
( k19_filter_2(sK1074,sF1078) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sF1078))
| ~ spl1087_389
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f18875,f18848]) ).
fof(f24036,plain,
( v1_xboole_0(sF1078)
| ~ m1_subset_1(sF1078,sF1086)
| spl1087_368 ),
inference(forward_subsumption_resolution,[],[f18893,f18372]) ).
fof(f24052,plain,
( k19_filter_2(sK1074,sF1078) = k19_filter_2(sK1074,k19_filter_2(sK1074,sF1078))
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f20077,f18848]) ).
fof(f24059,plain,
( m2_lattice4(sF1079,sK1074)
| ~ m1_subset_1(sF1078,sF1086)
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f20976,f18848]) ).
fof(f24060,plain,
( ~ v1_xboole_0(sF1079)
| ~ m1_subset_1(sF1078,sF1086)
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f21446,f18848]) ).
fof(f24076,plain,
( ~ m1_subset_1(sF1078,sF1086)
| v1_xboole_0(sF1078)
| spl1087_442 ),
inference(forward_subsumption_resolution,[],[f22842,f20450]) ).
fof(f24077,plain,
( k19_filter_2(sK1074,sF1078) = k3_filter_2(k1_lattice2(sK1074),sF1078)
| ~ spl1087_389
| spl1087_400 ),
inference(forward_demodulation,[],[f24035,f18171]) ).
fof(f24078,plain,
( ~ m1_subset_1(sF1078,sF1086)
| spl1087_368
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24036,f18848]) ).
fof(f24092,plain,
( sF1079 = k19_filter_2(sK1074,sF1079)
| spl1087_400 ),
inference(forward_demodulation,[],[f24052,f15432]) ).
fof(f24099,plain,
( m2_lattice4(sF1079,sK1074)
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24059,f18105]) ).
fof(f24100,plain,
( ~ v1_xboole_0(sF1079)
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24060,f18105]) ).
fof(f24116,plain,
( v1_xboole_0(sF1078)
| spl1087_442 ),
inference(forward_subsumption_resolution,[],[f24076,f18105]) ).
fof(f24118,plain,
( $false
| spl1087_368
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24078,f18105]) ).
fof(f24119,plain,
( spl1087_368
| spl1087_400 ),
inference(avatar_contradiction_clause,[],[f24118]) ).
fof(f24151,plain,
( $false
| spl1087_400
| spl1087_442 ),
inference(forward_subsumption_resolution,[],[f24116,f18848]) ).
fof(f24152,plain,
( spl1087_400
| spl1087_442 ),
inference(avatar_contradiction_clause,[],[f24151]) ).
fof(f24242,plain,
( sF1082 = k3_filter_2(k1_lattice2(sK1074),sF1081)
| ~ spl1087_355
| spl1087_381
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f23787,f15438]) ).
fof(f24249,definition,
( spl1087_526
<=> r1_tarski(sK1076,sF1081) ),
introduced(definition,[new_symbols(definition,[spl1087_526])],[avatar_definition]) ).
fof(f24250,plain,
( r1_tarski(sK1076,sF1081)
| ~ spl1087_526 ),
inference(avatar_component_clause,[],[f24249]) ).
fof(f24251,plain,
( ~ r1_tarski(sK1076,sF1081)
| spl1087_526 ),
inference(avatar_component_clause,[],[f24249]) ).
fof(f24263,definition,
( spl1087_529
<=> r1_tarski(sF1081,sK1076) ),
introduced(definition,[new_symbols(definition,[spl1087_529])],[avatar_definition]) ).
fof(f24264,plain,
( r1_tarski(sF1081,sK1076)
| ~ spl1087_529 ),
inference(avatar_component_clause,[],[f24263]) ).
fof(f24265,plain,
( ~ r1_tarski(sF1081,sK1076)
| spl1087_529 ),
inference(avatar_component_clause,[],[f24263]) ).
fof(f24293,plain,
( sF1079 = k3_filter_2(k1_lattice2(sK1074),sF1078)
| ~ spl1087_389
| spl1087_400 ),
inference(forward_demodulation,[],[f24077,f15432]) ).
fof(f24313,definition,
( spl1087_535
<=> r1_tarski(sK1075,sF1078) ),
introduced(definition,[new_symbols(definition,[spl1087_535])],[avatar_definition]) ).
fof(f24314,plain,
( r1_tarski(sK1075,sF1078)
| ~ spl1087_535 ),
inference(avatar_component_clause,[],[f24313]) ).
fof(f24315,plain,
( ~ r1_tarski(sK1075,sF1078)
| spl1087_535 ),
inference(avatar_component_clause,[],[f24313]) ).
fof(f24323,definition,
( spl1087_537
<=> r1_tarski(sF1078,sK1075) ),
introduced(definition,[new_symbols(definition,[spl1087_537])],[avatar_definition]) ).
fof(f24324,plain,
( r1_tarski(sF1078,sK1075)
| ~ spl1087_537 ),
inference(avatar_component_clause,[],[f24323]) ).
fof(f24325,plain,
( ~ r1_tarski(sF1078,sK1075)
| spl1087_537 ),
inference(avatar_component_clause,[],[f24323]) ).
fof(f24617,plain,
( r1_filter_2(sF1077,sF1079,sF1079)
| ~ m2_filter_2(sF1079,sK1074)
| spl1087_400 ),
inference(superposition,[],[f18110,f24092]) ).
fof(f24659,plain,
( r1_filter_2(sF1077,sF1079,sF1079)
| ~ spl1087_368
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24617,f18371]) ).
fof(f24753,plain,
( v1_xboole_0(sK1075)
| k3_filter_2(k1_lattice2(sK1074),sK1075) = k3_filter_0(k1_lattice2(sK1074),sK1075)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(resolution,[],[f23331,f15449]) ).
fof(f24754,plain,
( v1_xboole_0(sK1076)
| k3_filter_2(k1_lattice2(sK1074),sK1076) = k3_filter_0(k1_lattice2(sK1074),sK1076)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(resolution,[],[f23331,f15448]) ).
fof(f24756,plain,
( v1_xboole_0(sF1078)
| k3_filter_2(k1_lattice2(sK1074),sF1078) = k3_filter_0(k1_lattice2(sK1074),sF1078)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(resolution,[],[f23331,f18105]) ).
fof(f24758,plain,
( v1_xboole_0(sF1081)
| k3_filter_2(k1_lattice2(sK1074),sF1081) = k3_filter_0(k1_lattice2(sK1074),sF1081)
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(resolution,[],[f23331,f18094]) ).
fof(f24760,plain,
( v1_xboole_0(sF1084)
| k3_filter_0(k1_lattice2(sK1074),sF1084) = k3_filter_2(k1_lattice2(sK1074),sF1084)
| ~ spl1087_353
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(resolution,[],[f23331,f18080]) ).
fof(f24765,plain,
( k3_filter_2(k1_lattice2(sK1074),sF1081) = k3_filter_0(k1_lattice2(sK1074),sF1081)
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381 ),
inference(forward_subsumption_resolution,[],[f24758,f18722]) ).
fof(f24767,plain,
( k3_filter_2(k1_lattice2(sK1074),sF1078) = k3_filter_0(k1_lattice2(sK1074),sF1078)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24756,f18848]) ).
fof(f24769,plain,
( k3_filter_2(k1_lattice2(sK1074),sK1076) = k3_filter_0(k1_lattice2(sK1074),sK1076)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f24754,f13501]) ).
fof(f24770,plain,
( k3_filter_2(k1_lattice2(sK1074),sK1075) = k3_filter_0(k1_lattice2(sK1074),sK1075)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f24753,f13499]) ).
fof(f24776,plain,
( sF1082 = k3_filter_0(k1_lattice2(sK1074),sF1081)
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f24765,f24242]) ).
fof(f24778,plain,
( sF1079 = k3_filter_0(k1_lattice2(sK1074),sF1078)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389
| spl1087_400 ),
inference(forward_demodulation,[],[f24767,f24293]) ).
fof(f24780,plain,
( sF1083 = k3_filter_0(k1_lattice2(sK1074),sK1076)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f24769,f18883]) ).
fof(f24781,plain,
( sF1080 = k3_filter_0(k1_lattice2(sK1074),sK1075)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f24770,f18884]) ).
fof(f24788,plain,
( v3_struct_0(sK1074)
| ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| sF1079 = k7_filter_2(sK1074,sF1079)
| spl1087_400 ),
inference(resolution,[],[f24099,f18225]) ).
fof(f24793,plain,
( ~ v10_lattices(sK1074)
| ~ l3_lattices(sK1074)
| sF1079 = k7_filter_2(sK1074,sF1079)
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24788,f13497]) ).
fof(f24796,plain,
( ~ l3_lattices(sK1074)
| sF1079 = k7_filter_2(sK1074,sF1079)
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24793,f13496]) ).
fof(f24799,plain,
( sF1079 = k7_filter_2(sK1074,sF1079)
| spl1087_400 ),
inference(forward_subsumption_resolution,[],[f24796,f13495]) ).
fof(f25344,definition,
( spl1087_601
<=> sF1079 = sF1082 ),
introduced(definition,[new_symbols(definition,[spl1087_601])],[avatar_definition]) ).
fof(f25346,plain,
( sF1079 = sF1082
| ~ spl1087_601 ),
inference(avatar_component_clause,[],[f25344]) ).
fof(f25545,plain,
( v1_xboole_0(sF1079)
| k19_filter_2(sK1074,sF1079) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sF1079))
| ~ spl1087_389
| ~ spl1087_442 ),
inference(resolution,[],[f20449,f18781]) ).
fof(f25587,plain,
( v1_xboole_0(sF1079)
| k3_filter_0(k1_lattice2(sK1074),sF1079) = k3_filter_2(k1_lattice2(sK1074),sF1079)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_442 ),
inference(resolution,[],[f20449,f23331]) ).
fof(f25590,plain,
( k3_filter_0(k1_lattice2(sK1074),sF1079) = k3_filter_2(k1_lattice2(sK1074),sF1079)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_400
| ~ spl1087_442 ),
inference(forward_subsumption_resolution,[],[f25587,f24100]) ).
fof(f25620,plain,
( k19_filter_2(sK1074,sF1079) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sF1079))
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442 ),
inference(forward_subsumption_resolution,[],[f25545,f24100]) ).
fof(f25644,plain,
( k19_filter_2(sK1074,sF1079) = k3_filter_2(k1_lattice2(sK1074),sF1079)
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442 ),
inference(forward_demodulation,[],[f25620,f24799]) ).
fof(f25657,plain,
( k19_filter_2(sK1074,sF1079) = k3_filter_0(k1_lattice2(sK1074),sF1079)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442 ),
inference(forward_demodulation,[],[f25644,f25590]) ).
fof(f25658,plain,
( sF1079 = k3_filter_0(k1_lattice2(sK1074),sF1079)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442 ),
inference(forward_demodulation,[],[f25657,f24092]) ).
fof(f27616,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,k3_filter_0(k1_lattice2(sK1074),X0)))
| v1_xboole_0(sK1075) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(resolution,[],[f23414,f15449]) ).
fof(f27637,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,k3_filter_0(k1_lattice2(sK1074),X0))) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f27616,f13499]) ).
fof(f27655,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,k3_filter_0(k1_lattice2(sK1074),sK1075),X0))
| v1_xboole_0(sK1075) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(resolution,[],[f23413,f15449]) ).
fof(f27676,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1086)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,k3_filter_0(k1_lattice2(sK1074),sK1075),X0)) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f27655,f13499]) ).
fof(f27684,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1086)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,X0)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sF1080,X0))
| v1_xboole_0(X0) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f27676,f24781]) ).
fof(f27699,plain,
( k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,sK1076)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sF1080,sK1076))
| v1_xboole_0(sK1076)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(resolution,[],[f27684,f15448]) ).
fof(f27718,plain,
( k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,sK1076)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sF1080,sK1076))
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_subsumption_resolution,[],[f27699,f13501]) ).
fof(f27731,plain,
( k3_filter_0(k1_lattice2(sK1074),sF1081) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,sK1076))
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f27718,f15436]) ).
fof(f27740,plain,
( k3_filter_0(k1_lattice2(sK1074),sF1078) = k3_filter_0(k1_lattice2(sK1074),sF1081)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f27731,f15430]) ).
fof(f27747,plain,
( sF1082 = k3_filter_0(k1_lattice2(sK1074),sF1078)
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f27740,f24776]) ).
fof(f27751,plain,
( sF1079 = sF1082
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| ~ spl1087_389
| spl1087_400 ),
inference(forward_demodulation,[],[f27747,f24778]) ).
fof(f27754,plain,
( spl1087_601
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| ~ spl1087_389
| spl1087_400 ),
inference(avatar_split_clause,[],[f27751,f18847,f18780,f18721,f18309,f18305,f18301,f18092,f25344]) ).
fof(f27756,plain,
( ~ r1_filter_2(sF1077,sF1079,sF1079)
| spl1087_2
| ~ spl1087_601 ),
inference(superposition,[],[f15515,f25346]) ).
fof(f27787,plain,
( $false
| spl1087_2
| ~ spl1087_368
| spl1087_400
| ~ spl1087_601 ),
inference(forward_subsumption_resolution,[],[f27756,f24659]) ).
fof(f27788,plain,
( spl1087_2
| ~ spl1087_368
| spl1087_400
| ~ spl1087_601 ),
inference(avatar_contradiction_clause,[],[f27787]) ).
fof(f28264,plain,
( v1_xboole_0(sK1076)
| k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,sK1076)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,k3_filter_0(k1_lattice2(sK1074),sK1076)))
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(resolution,[],[f27637,f15448]) ).
fof(f28281,plain,
( k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,sK1076)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,k3_filter_0(k1_lattice2(sK1074),sK1076)))
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f28264,f13501]) ).
fof(f28288,plain,
( k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,sK1076)) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,sF1083))
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f28281,f24780]) ).
fof(f28291,plain,
( k3_filter_0(k1_lattice2(sK1074),sF1084) = k3_filter_0(k1_lattice2(sK1074),k4_subset_1(sF1077,sK1075,sK1076))
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f28288,f15442]) ).
fof(f28294,plain,
( k3_filter_0(k1_lattice2(sK1074),sF1078) = k3_filter_0(k1_lattice2(sK1074),sF1084)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f28291,f15430]) ).
fof(f36105,definition,
( spl1087_1508
<=> sF1079 = sF1085 ),
introduced(definition,[new_symbols(definition,[spl1087_1508])],[avatar_definition]) ).
fof(f36106,plain,
( sF1079 != sF1085
| spl1087_1508 ),
inference(avatar_component_clause,[],[f36105]) ).
fof(f36107,plain,
( sF1079 = sF1085
| ~ spl1087_1508 ),
inference(avatar_component_clause,[],[f36105]) ).
fof(f36790,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v3_struct_0(k1_lattice2(sK1074))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(X0)
| m1_filter_0(k3_filter_0(k1_lattice2(sK1074),X0),k1_lattice2(sK1074)) ),
inference(superposition,[],[f12684,f18286]) ).
fof(f36796,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ v10_lattices(k1_lattice2(sK1074))
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(X0)
| m1_filter_0(k3_filter_0(k1_lattice2(sK1074),X0),k1_lattice2(sK1074)) )
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f36790,f18310]) ).
fof(f36803,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| ~ l3_lattices(k1_lattice2(sK1074))
| v1_xboole_0(X0)
| m1_filter_0(k3_filter_0(k1_lattice2(sK1074),X0),k1_lattice2(sK1074)) )
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f36796,f18306]) ).
fof(f36806,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1077))
| v1_xboole_0(X0)
| m1_filter_0(k3_filter_0(k1_lattice2(sK1074),X0),k1_lattice2(sK1074)) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_subsumption_resolution,[],[f36803,f18302]) ).
fof(f36808,plain,
( ! [X0] :
( m1_filter_0(k3_filter_0(k1_lattice2(sK1074),X0),k1_lattice2(sK1074))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1086) )
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362 ),
inference(forward_demodulation,[],[f36806,f15447]) ).
fof(f39640,plain,
( m1_filter_0(sF1079,k1_lattice2(sK1074))
| v1_xboole_0(sF1079)
| ~ m1_subset_1(sF1079,sF1086)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442 ),
inference(superposition,[],[f36808,f25658]) ).
fof(f39647,plain,
( m1_filter_0(sF1079,k1_lattice2(sK1074))
| ~ m1_subset_1(sF1079,sF1086)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442 ),
inference(forward_subsumption_resolution,[],[f39640,f24100]) ).
fof(f39673,plain,
( m1_filter_0(sF1079,k1_lattice2(sK1074))
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442 ),
inference(forward_subsumption_resolution,[],[f39647,f20449]) ).
fof(f39730,plain,
( r1_filter_2(sF1077,sF1079,sF1079)
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_375
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442 ),
inference(resolution,[],[f39673,f23410]) ).
fof(f45414,plain,
( r1_tarski(k3_subset_1(sF1077,k3_tarski(k2_tarski(sK1076,sF1080))),k3_subset_1(sF1077,sK1076))
| ~ m1_subset_1(sF1080,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ spl1087_356 ),
inference(superposition,[],[f8734,f20570]) ).
fof(f45417,plain,
( r1_tarski(k3_subset_1(sF1077,sF1081),k3_subset_1(sF1077,sK1076))
| ~ m1_subset_1(sF1080,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ spl1087_356 ),
inference(forward_demodulation,[],[f45414,f20641]) ).
fof(f45424,plain,
( ~ m1_subset_1(sF1080,sF1086)
| r1_tarski(k3_subset_1(sF1077,sF1081),k3_subset_1(sF1077,sK1076))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ spl1087_356 ),
inference(forward_demodulation,[],[f45417,f15447]) ).
fof(f45429,plain,
( r1_tarski(k3_subset_1(sF1077,sF1081),k3_subset_1(sF1077,sK1076))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ spl1087_356 ),
inference(forward_subsumption_resolution,[],[f45424,f18097]) ).
fof(f45433,plain,
( ~ m1_subset_1(sK1076,sF1086)
| r1_tarski(k3_subset_1(sF1077,sF1081),k3_subset_1(sF1077,sK1076))
| ~ spl1087_356 ),
inference(forward_demodulation,[],[f45429,f15447]) ).
fof(f45436,plain,
( r1_tarski(k3_subset_1(sF1077,sF1081),k3_subset_1(sF1077,sK1076))
| ~ spl1087_356 ),
inference(forward_subsumption_resolution,[],[f45433,f15448]) ).
fof(f46184,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ v1_xboole_0(X0) ),
inference(resolution,[],[f8160,f8047]) ).
fof(f66739,plain,
( ~ v1_xboole_0(sF1078)
| spl1087_537 ),
inference(resolution,[],[f46184,f24325]) ).
fof(f66769,plain,
( ~ v1_xboole_0(sF1081)
| spl1087_529 ),
inference(resolution,[],[f46184,f24265]) ).
fof(f66794,plain,
( $false
| ~ spl1087_381
| spl1087_529 ),
inference(forward_subsumption_resolution,[],[f66769,f18723]) ).
fof(f66795,plain,
( ~ spl1087_381
| spl1087_529 ),
inference(avatar_contradiction_clause,[],[f66794]) ).
fof(f66824,plain,
( ~ r1_tarski(sK1076,sF1081)
| sK1076 = sF1081
| ~ spl1087_529 ),
inference(resolution,[],[f24264,f8115]) ).
fof(f74904,plain,
( r1_tarski(sK1075,sF1078)
| ~ m1_subset_1(sF1078,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077)) ),
inference(resolution,[],[f8723,f18490]) ).
fof(f74907,plain,
( r1_tarski(sK1076,sF1081)
| ~ m1_subset_1(sF1081,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ spl1087_356 ),
inference(resolution,[],[f8723,f45436]) ).
fof(f74909,plain,
( r1_tarski(sF1083,sF1084)
| ~ m1_subset_1(sF1084,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077))
| ~ spl1087_354 ),
inference(resolution,[],[f8723,f20859]) ).
fof(f74946,plain,
( ~ m1_subset_1(sF1084,sF1086)
| r1_tarski(sF1083,sF1084)
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077))
| ~ spl1087_354 ),
inference(forward_demodulation,[],[f74909,f15447]) ).
fof(f74948,plain,
( ~ m1_subset_1(sF1081,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ spl1087_356
| spl1087_526 ),
inference(forward_subsumption_resolution,[],[f74907,f24251]) ).
fof(f74951,plain,
( ~ m1_subset_1(sF1078,k1_zfmisc_1(sF1077))
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077))
| spl1087_535 ),
inference(forward_subsumption_resolution,[],[f74904,f24315]) ).
fof(f74969,plain,
( r1_tarski(sF1083,sF1084)
| ~ m1_subset_1(sF1083,k1_zfmisc_1(sF1077))
| ~ spl1087_353
| ~ spl1087_354 ),
inference(forward_subsumption_resolution,[],[f74946,f18080]) ).
fof(f74971,plain,
( ~ m1_subset_1(sF1081,sF1086)
| ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ spl1087_356
| spl1087_526 ),
inference(forward_demodulation,[],[f74948,f15447]) ).
fof(f74974,plain,
( ~ m1_subset_1(sF1078,sF1086)
| ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077))
| spl1087_535 ),
inference(forward_demodulation,[],[f74951,f15447]) ).
fof(f74991,plain,
( ~ m1_subset_1(sF1083,sF1086)
| r1_tarski(sF1083,sF1084)
| ~ spl1087_353
| ~ spl1087_354 ),
inference(forward_demodulation,[],[f74969,f15447]) ).
fof(f74993,plain,
( ~ m1_subset_1(sK1076,k1_zfmisc_1(sF1077))
| ~ spl1087_355
| ~ spl1087_356
| spl1087_526 ),
inference(forward_subsumption_resolution,[],[f74971,f18094]) ).
fof(f74996,plain,
( ~ m1_subset_1(sK1075,k1_zfmisc_1(sF1077))
| spl1087_535 ),
inference(forward_subsumption_resolution,[],[f74974,f18105]) ).
fof(f74999,plain,
( r1_tarski(sF1083,sF1084)
| ~ spl1087_353
| ~ spl1087_354 ),
inference(forward_subsumption_resolution,[],[f74991,f18083]) ).
fof(f75001,plain,
( ~ m1_subset_1(sK1076,sF1086)
| ~ spl1087_355
| ~ spl1087_356
| spl1087_526 ),
inference(forward_demodulation,[],[f74993,f15447]) ).
fof(f75004,plain,
( ~ m1_subset_1(sK1075,sF1086)
| spl1087_535 ),
inference(forward_demodulation,[],[f74996,f15447]) ).
fof(f75008,plain,
( $false
| ~ spl1087_355
| ~ spl1087_356
| spl1087_526 ),
inference(forward_subsumption_resolution,[],[f75001,f15448]) ).
fof(f75009,plain,
( ~ spl1087_355
| ~ spl1087_356
| spl1087_526 ),
inference(avatar_contradiction_clause,[],[f75008]) ).
fof(f75013,plain,
( $false
| spl1087_535 ),
inference(forward_subsumption_resolution,[],[f75004,f15449]) ).
fof(f75014,plain,
spl1087_535,
inference(avatar_contradiction_clause,[],[f75013]) ).
fof(f75059,plain,
( sK1076 = sF1081
| ~ spl1087_526
| ~ spl1087_529 ),
inference(forward_subsumption_resolution,[],[f66824,f24250]) ).
fof(f75547,plain,
( ~ r1_tarski(sF1078,sK1075)
| sK1075 = sF1078
| ~ spl1087_535 ),
inference(resolution,[],[f24314,f8115]) ).
fof(f75654,plain,
( ~ v1_xboole_0(sF1081)
| ~ spl1087_526
| ~ spl1087_529 ),
inference(superposition,[],[f13501,f75059]) ).
fof(f76169,plain,
( $false
| ~ spl1087_381
| ~ spl1087_526
| ~ spl1087_529 ),
inference(forward_subsumption_resolution,[],[f75654,f18723]) ).
fof(f76170,plain,
( ~ spl1087_381
| ~ spl1087_526
| ~ spl1087_529 ),
inference(avatar_contradiction_clause,[],[f76169]) ).
fof(f77458,plain,
( $false
| ~ spl1087_400
| spl1087_537 ),
inference(forward_subsumption_resolution,[],[f66739,f18849]) ).
fof(f77459,plain,
( ~ spl1087_400
| spl1087_537 ),
inference(avatar_contradiction_clause,[],[f77458]) ).
fof(f80612,plain,
( sK1075 = sF1078
| ~ spl1087_535
| ~ spl1087_537 ),
inference(forward_subsumption_resolution,[],[f75547,f24324]) ).
fof(f80816,plain,
( sF1082 = k3_filter_0(k1_lattice2(sK1074),sF1084)
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f28294,f27747]) ).
fof(f83844,plain,
( ~ v1_xboole_0(sF1078)
| ~ spl1087_535
| ~ spl1087_537 ),
inference(superposition,[],[f13499,f80612]) ).
fof(f84242,plain,
( $false
| ~ spl1087_400
| ~ spl1087_535
| ~ spl1087_537 ),
inference(forward_subsumption_resolution,[],[f83844,f18849]) ).
fof(f84243,plain,
( ~ spl1087_400
| ~ spl1087_535
| ~ spl1087_537 ),
inference(avatar_contradiction_clause,[],[f84242]) ).
fof(f113934,plain,
( k19_filter_2(sK1074,sF1084) = k3_filter_2(k1_lattice2(sK1074),k7_filter_2(sK1074,sF1084))
| ~ spl1087_353
| spl1087_383
| ~ spl1087_389 ),
inference(forward_subsumption_resolution,[],[f20826,f18731]) ).
fof(f115730,plain,
( k19_filter_2(sK1074,sF1084) = k3_filter_2(k1_lattice2(sK1074),sF1084)
| ~ spl1087_353
| spl1087_383
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f113934,f20820]) ).
fof(f130656,plain,
( k3_filter_0(k1_lattice2(sK1074),sF1084) = k3_filter_2(k1_lattice2(sK1074),sF1084)
| ~ spl1087_353
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_383 ),
inference(forward_subsumption_resolution,[],[f24760,f18731]) ).
fof(f130792,plain,
( sF1085 = k3_filter_2(k1_lattice2(sK1074),sF1084)
| ~ spl1087_353
| spl1087_383
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f115730,f15444]) ).
fof(f130932,definition,
( spl1087_4009
<=> r1_tarski(sF1084,sF1083) ),
introduced(definition,[new_symbols(definition,[spl1087_4009])],[avatar_definition]) ).
fof(f130933,plain,
( r1_tarski(sF1084,sF1083)
| ~ spl1087_4009 ),
inference(avatar_component_clause,[],[f130932]) ).
fof(f130934,plain,
( ~ r1_tarski(sF1084,sF1083)
| spl1087_4009 ),
inference(avatar_component_clause,[],[f130932]) ).
fof(f131128,plain,
( sF1085 = k3_filter_0(k1_lattice2(sK1074),sF1084)
| ~ spl1087_353
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_383
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f130792,f130656]) ).
fof(f133082,plain,
( ~ v1_xboole_0(sF1084)
| spl1087_4009 ),
inference(resolution,[],[f130934,f46184]) ).
fof(f134182,plain,
( ~ r1_tarski(sF1083,sF1084)
| sF1083 = sF1084
| ~ spl1087_4009 ),
inference(resolution,[],[f130933,f8115]) ).
fof(f134183,plain,
( sF1083 = sF1084
| ~ spl1087_353
| ~ spl1087_354
| ~ spl1087_4009 ),
inference(forward_subsumption_resolution,[],[f134182,f74999]) ).
fof(f134189,plain,
( v1_xboole_0(sF1083)
| ~ spl1087_353
| ~ spl1087_354
| ~ spl1087_383
| ~ spl1087_4009 ),
inference(superposition,[],[f18732,f134183]) ).
fof(f134244,plain,
( $false
| ~ spl1087_353
| ~ spl1087_354
| ~ spl1087_383
| ~ spl1087_393
| ~ spl1087_4009 ),
inference(forward_subsumption_resolution,[],[f134189,f19643]) ).
fof(f134245,plain,
( ~ spl1087_353
| ~ spl1087_354
| ~ spl1087_383
| ~ spl1087_393
| ~ spl1087_4009 ),
inference(avatar_contradiction_clause,[],[f134244]) ).
fof(f144000,plain,
( ~ spl1087_383
| spl1087_4009 ),
inference(avatar_split_clause,[],[f133082,f130932,f18730]) ).
fof(f144060,plain,
( sF1082 = sF1085
| ~ spl1087_353
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| spl1087_383
| ~ spl1087_389 ),
inference(forward_demodulation,[],[f80816,f131128]) ).
fof(f146677,plain,
( ~ r1_filter_2(sF1077,sF1079,sF1079)
| spl1087_1
| ~ spl1087_1508 ),
inference(superposition,[],[f15511,f36107]) ).
fof(f146706,plain,
( $false
| spl1087_1
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_375
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442
| ~ spl1087_1508 ),
inference(forward_subsumption_resolution,[],[f146677,f39730]) ).
fof(f146707,plain,
( spl1087_1
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_375
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442
| ~ spl1087_1508 ),
inference(avatar_contradiction_clause,[],[f146706]) ).
fof(f146718,plain,
( sF1079 = sF1085
| ~ spl1087_353
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| spl1087_383
| ~ spl1087_389
| ~ spl1087_601 ),
inference(forward_demodulation,[],[f144060,f25346]) ).
fof(f146777,plain,
( $false
| ~ spl1087_353
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| spl1087_383
| ~ spl1087_389
| ~ spl1087_601
| spl1087_1508 ),
inference(forward_subsumption_resolution,[],[f146718,f36106]) ).
fof(f146778,plain,
( ~ spl1087_353
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| spl1087_383
| ~ spl1087_389
| ~ spl1087_601
| spl1087_1508 ),
inference(avatar_contradiction_clause,[],[f146777]) ).
cnf(s1,plain,
( ~ spl1087_1
| ~ spl1087_2 ),
inference(sat_conversion,[],[f15516]) ).
cnf(s301,plain,
( spl1087_353
| ~ spl1087_354 ),
inference(sat_conversion,[],[f18085]) ).
cnf(s302,plain,
( spl1087_355
| ~ spl1087_356 ),
inference(sat_conversion,[],[f18099]) ).
cnf(s311,plain,
spl1087_359,
inference(sat_conversion,[],[f18345]) ).
cnf(s315,plain,
spl1087_360,
inference(sat_conversion,[],[f18506]) ).
cnf(s317,plain,
~ spl1087_362,
inference(sat_conversion,[],[f18517]) ).
cnf(s324,plain,
( ~ spl1087_359
| ~ spl1087_375 ),
inference(sat_conversion,[],[f18694]) ).
cnf(s329,plain,
( spl1087_388
| spl1087_389 ),
inference(sat_conversion,[],[f18782]) ).
cnf(s342,plain,
~ spl1087_388,
inference(sat_conversion,[],[f18870]) ).
cnf(s343,plain,
spl1087_393,
inference(sat_conversion,[],[f18911]) ).
cnf(s344,plain,
spl1087_391,
inference(sat_conversion,[],[f18913]) ).
cnf(s371,plain,
( spl1087_356
| ~ spl1087_391 ),
inference(sat_conversion,[],[f20551]) ).
cnf(s373,plain,
( spl1087_354
| ~ spl1087_393 ),
inference(sat_conversion,[],[f20717]) ).
cnf(s420,plain,
spl1087_361,
inference(sat_conversion,[],[f23100]) ).
cnf(s445,plain,
( spl1087_368
| spl1087_400 ),
inference(sat_conversion,[],[f24119]) ).
cnf(s446,plain,
( spl1087_400
| spl1087_442 ),
inference(sat_conversion,[],[f24152]) ).
cnf(s714,plain,
( ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| ~ spl1087_389
| spl1087_400
| spl1087_601 ),
inference(sat_conversion,[],[f27754]) ).
cnf(s717,plain,
( spl1087_2
| ~ spl1087_368
| spl1087_400
| ~ spl1087_601 ),
inference(sat_conversion,[],[f27788]) ).
cnf(s3074,plain,
( ~ spl1087_381
| spl1087_529 ),
inference(sat_conversion,[],[f66795]) ).
cnf(s3588,plain,
( ~ spl1087_355
| ~ spl1087_356
| spl1087_526 ),
inference(sat_conversion,[],[f75009]) ).
cnf(s3591,plain,
spl1087_535,
inference(sat_conversion,[],[f75014]) ).
cnf(s3655,plain,
( ~ spl1087_381
| ~ spl1087_526
| ~ spl1087_529 ),
inference(sat_conversion,[],[f76170]) ).
cnf(s3725,plain,
( ~ spl1087_400
| spl1087_537 ),
inference(sat_conversion,[],[f77459]) ).
cnf(s4038,plain,
( ~ spl1087_400
| ~ spl1087_535
| ~ spl1087_537 ),
inference(sat_conversion,[],[f84243]) ).
cnf(s4659,plain,
( ~ spl1087_353
| ~ spl1087_354
| ~ spl1087_383
| ~ spl1087_393
| ~ spl1087_4009 ),
inference(sat_conversion,[],[f134245]) ).
cnf(s4849,plain,
( ~ spl1087_383
| spl1087_4009 ),
inference(sat_conversion,[],[f144000]) ).
cnf(s4954,plain,
( spl1087_1
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_375
| ~ spl1087_389
| spl1087_400
| ~ spl1087_442
| ~ spl1087_1508 ),
inference(sat_conversion,[],[f146707]) ).
cnf(s4965,plain,
( ~ spl1087_353
| ~ spl1087_355
| ~ spl1087_360
| ~ spl1087_361
| spl1087_362
| spl1087_381
| spl1087_383
| ~ spl1087_389
| ~ spl1087_601
| spl1087_1508 ),
inference(sat_conversion,[],[f146778]) ).
cnf(s5210,plain,
spl1087_356,
inference(rat,[],[s371,s344]) ).
cnf(s5216,plain,
spl1087_354,
inference(rat,[],[s373,s343]) ).
cnf(s5233,plain,
spl1087_389,
inference(rat,[],[s329,s342]) ).
cnf(s5633,plain,
~ spl1087_375,
inference(rat,[],[s324,s311]) ).
cnf(s5794,plain,
spl1087_355,
inference(rat,[],[s302,s5210]) ).
cnf(s5795,plain,
spl1087_526,
inference(rat,[],[s3588,s5210,s5794]) ).
cnf(s5798,plain,
spl1087_353,
inference(rat,[],[s301,s5216]) ).
cnf(s5813,plain,
~ spl1087_400,
inference(rat,[],[s3725,s4038,s3591]) ).
cnf(s5823,plain,
spl1087_442,
inference(rat,[],[s446,s5813]) ).
cnf(s5824,plain,
spl1087_368,
inference(rat,[],[s445,s5813]) ).
cnf(s5976,plain,
~ spl1087_381,
inference(rat,[],[s3074,s3655,s5795]) ).
cnf(s6247,plain,
spl1087_601,
inference(rat,[],[s714,s5813,s5794,s5233,s315,s317,s420,s5976]) ).
cnf(s6248,plain,
~ spl1087_383,
inference(rat,[],[s4659,s4849,s5216,s343,s5798]) ).
cnf(s6290,plain,
spl1087_2,
inference(rat,[],[s717,s5824,s5813,s6247]) ).
cnf(s6291,plain,
spl1087_1508,
inference(rat,[],[s4965,s6248,s5976,s5233,s5798,s5794,s317,s420,s315,s6247]) ).
cnf(s6299,plain,
~ spl1087_1,
inference(rat,[],[s1,s6290]) ).
cnf(s6301,plain,
$false,
inference(rat,[],[s4954,s5823,s5813,s5633,s5233,s315,s317,s420,s6299,s6291]) ).
fof(f146827,plain,
$false,
inference(avatar_sat_refutation,[],[s6301]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT315+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n010.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 14:32:48 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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.11/2.57 % (1020438)Detected formulas, will run a generic FOF schedule.
% 11.11/2.57 % (1020447)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4256039431:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 11.11/2.57 % (1020447)Instruction limit reached!
% 11.11/2.57 % (1020447)------------------------------
% 11.11/2.57 % (1020447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.57 % (1020447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.57 % (1020447)CaDiCaL version: 2.1.3
% 11.11/2.57 % (1020447)Termination reason: Instruction limit
% 11.11/2.57 % (1020447)Termination phase: Saturation
% 11.11/2.57 % (1020445)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=567575244:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 11.11/2.57 % (1020447)Time elapsed: 0.045 s
% 11.11/2.57 % (1020446)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3754964859:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 11.11/2.57 % (1020447)Peak memory usage: 92 MB
% 11.11/2.57 % (1020444)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=3062175506:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 11.11/2.57 % (1020447)Instructions burned: 120 (million)
% 11.11/2.57 % (1020443)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=2803951607:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 11.11/2.57 % (1020449)dis-21_1_sil=8000:lcm=predicate:random_seed=1270023505:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 11.11/2.57 % (1020446)Refutation not found, incomplete strategy
% 11.11/2.57 % (1020446)------------------------------
% 11.11/2.57 % (1020446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.57 % (1020446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.57 % (1020446)CaDiCaL version: 2.1.3
% 11.11/2.57 % (1020446)Termination reason: Refutation not found, incomplete strategy
% 11.11/2.57 % (1020446)Time elapsed: 0.020 s
% 11.11/2.57 % (1020446)Peak memory usage: 92 MB
% 11.11/2.57 % (1020446)Instructions burned: 26 (million)
% 11.11/2.57 % (1020448)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3740334916:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 11.11/2.57 % (1020449)Instruction limit reached!
% 11.11/2.57 % (1020449)------------------------------
% 11.11/2.57 % (1020449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.57 % (1020449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.57 % (1020449)CaDiCaL version: 2.1.3
% 11.11/2.57 % (1020449)Termination reason: Instruction limit
% 11.11/2.57 % (1020449)Termination phase: Property scanning
% 11.11/2.57 % (1020449)Time elapsed: 0.081 s
% 11.11/2.57 % (1020449)Peak memory usage: 92 MB
% 11.11/2.57 % (1020449)Instructions burned: 129 (million)
% 11.11/2.57 % (1020455)lrs+10_1_sil=8000:sp=occurrence:random_seed=2496173899:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.11/2.57 % (1020448)Instruction limit reached!
% 11.11/2.57 % (1020448)------------------------------
% 11.11/2.57 % (1020448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.57 % (1020448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.57 % (1020448)CaDiCaL version: 2.1.3
% 11.11/2.57 % (1020448)Termination reason: Instruction limit
% 11.11/2.57 % (1020448)Termination phase: Property scanning
% 11.11/2.57 % (1020448)Time elapsed: 0.090 s
% 11.11/2.57 % (1020448)Peak memory usage: 94 MB
% 11.11/2.57 % (1020448)Instructions burned: 141 (million)
% 11.11/2.57 % (1020455)Instruction limit reached!
% 11.11/2.57 % (1020455)------------------------------
% 11.11/2.57 % (1020455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.57 % (1020455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.57 % (1020455)CaDiCaL version: 2.1.3
% 11.11/2.57 % (1020455)Termination reason: Instruction limit
% 11.11/2.57 % (1020455)Termination phase: Saturation
% 11.11/2.57 % (1020455)Time elapsed: 0.106 s
% 11.11/2.57 % (1020455)Peak memory usage: 95 MB
% 11.11/2.57 % (1020455)Instructions burned: 285 (million)
% 18.45/3.63 % (1020459)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1196685108:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 18.45/3.63 % (1020460)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3199886541:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 18.45/3.63 % (1020446)------------------------------
% 18.45/3.63 % (1020446)------------------------------
% 18.45/3.63 % (1020461)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=313743175:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 18.45/3.63 % (1020459)Instruction limit reached!
% 18.45/3.63 % (1020459)------------------------------
% 18.45/3.63 % (1020459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.45/3.63 % (1020459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.45/3.63 % (1020459)CaDiCaL version: 2.1.3
% 18.45/3.63 % (1020459)Termination reason: Instruction limit
% 18.45/3.63 % (1020459)Termination phase: Saturation
% 18.45/3.63 % (1020459)Time elapsed: 0.085 s
% 18.45/3.63 % (1020459)Peak memory usage: 93 MB
% 18.45/3.63 % (1020459)Instructions burned: 159 (million)
% 18.45/3.63 % (1020461)Instruction limit reached!
% 18.45/3.63 % (1020461)------------------------------
% 18.45/3.63 % (1020461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.45/3.63 % (1020461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.45/3.63 % (1020461)CaDiCaL version: 2.1.3
% 18.45/3.63 % (1020461)Termination reason: Instruction limit
% 18.45/3.63 % (1020461)Termination phase: Saturation
% 18.45/3.63 % (1020461)Time elapsed: 0.076 s
% 18.45/3.63 % (1020461)Peak memory usage: 98 MB
% 18.45/3.63 % (1020461)Instructions burned: 248 (million)
% 18.45/3.63 % (1020464)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2880157972:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 18.45/3.63 % (1020466)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2371075655:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 18.45/3.63 % (1020467)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1129284713:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 18.45/3.63 % (1020460)Instruction limit reached!
% 18.45/3.63 % (1020460)------------------------------
% 18.45/3.63 % (1020460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.45/3.63 % (1020460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.45/3.63 % (1020460)CaDiCaL version: 2.1.3
% 18.45/3.63 % (1020460)Termination reason: Instruction limit
% 18.45/3.63 % (1020460)Termination phase: Saturation
% 18.45/3.63 % (1020460)Time elapsed: 0.213 s
% 18.45/3.63 % (1020460)Peak memory usage: 94 MB
% 18.45/3.63 % (1020460)Instructions burned: 326 (million)
% 18.45/3.63 % (1020467)Instruction limit reached!
% 18.45/3.63 % (1020467)------------------------------
% 18.45/3.63 % (1020467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.45/3.63 % (1020467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.45/3.63 % (1020467)CaDiCaL version: 2.1.3
% 18.45/3.63 % (1020467)Termination reason: Instruction limit
% 18.45/3.63 % (1020467)Termination phase: Saturation
% 18.45/3.63 % (1020467)Time elapsed: 0.033 s
% 18.45/3.63 % (1020467)Peak memory usage: 93 MB
% 18.45/3.63 % (1020467)Instructions burned: 116 (million)
% 18.45/3.63 % (1020472)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=477172608:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 18.45/3.63 % (1020464)Instruction limit reached!
% 18.45/3.63 % (1020464)------------------------------
% 18.45/3.63 % (1020464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.45/3.63 % (1020464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.45/3.63 % (1020464)CaDiCaL version: 2.1.3
% 18.45/3.63 % (1020464)Termination reason: Instruction limit
% 18.45/3.63 % (1020464)Termination phase: Saturation
% 18.45/3.63 % (1020464)Time elapsed: 0.166 s
% 18.45/3.63 % (1020464)Peak memory usage: 95 MB
% 18.45/3.63 % (1020464)Instructions burned: 295 (million)
% 18.45/3.63 % (1020471)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3126748202:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 18.45/3.63 % (1020472)Instruction limit reached!
% 18.45/3.63 % (1020472)------------------------------
% 18.45/3.63 % (1020472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.83 % (1020472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.83 % (1020472)CaDiCaL version: 2.1.3
% 40.97/6.83 % (1020472)Termination reason: Instruction limit
% 40.97/6.83 % (1020472)Termination phase: Property scanning
% 40.97/6.83 % (1020472)Time elapsed: 0.032 s
% 40.97/6.83 % (1020472)Peak memory usage: 91 MB
% 40.97/6.83 % (1020472)Instructions burned: 116 (million)
% 40.97/6.83 % (1020471)Instruction limit reached!
% 40.97/6.83 % (1020471)------------------------------
% 40.97/6.83 % (1020471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.83 % (1020471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.83 % (1020471)CaDiCaL version: 2.1.3
% 40.97/6.83 % (1020471)Termination reason: Instruction limit
% 40.97/6.83 % (1020471)Termination phase: Property scanning
% 40.97/6.83 % (1020471)Time elapsed: 0.078 s
% 40.97/6.83 % (1020471)Peak memory usage: 94 MB
% 40.97/6.83 % (1020471)Instructions burned: 129 (million)
% 40.97/6.83 % (1020476)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1257535930:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 40.97/6.83 % (1020474)lrs+10_1_sil=8000:sp=occurrence:random_seed=3613913159:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 40.97/6.83 % (1020477)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4119309305:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 40.97/6.83 % (1020476)Instruction limit reached!
% 40.97/6.83 % (1020476)------------------------------
% 40.97/6.83 % (1020476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.83 % (1020476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.83 % (1020476)CaDiCaL version: 2.1.3
% 40.97/6.83 % (1020476)Termination reason: Instruction limit
% 40.97/6.83 % (1020476)Termination phase: Saturation
% 40.97/6.83 % (1020476)Time elapsed: 0.135 s
% 40.97/6.83 % (1020476)Peak memory usage: 97 MB
% 40.97/6.83 % (1020476)Instructions burned: 441 (million)
% 40.97/6.83 % (1020481)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2763868554:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 40.97/6.83 % (1020481)Instruction limit reached!
% 40.97/6.83 % (1020481)------------------------------
% 40.97/6.83 % (1020481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.83 % (1020481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.83 % (1020481)CaDiCaL version: 2.1.3
% 40.97/6.83 % (1020481)Termination reason: Instruction limit
% 40.97/6.83 % (1020481)Termination phase: Saturation
% 40.97/6.83 % (1020481)Time elapsed: 0.045 s
% 40.97/6.83 % (1020481)Peak memory usage: 94 MB
% 40.97/6.83 % (1020481)Instructions burned: 137 (million)
% 40.97/6.83 % (1020483)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4293397407:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 40.97/6.83 % (1020483)Instruction limit reached!
% 40.97/6.83 % (1020483)------------------------------
% 40.97/6.83 % (1020483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.83 % (1020483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.83 % (1020483)CaDiCaL version: 2.1.3
% 40.97/6.83 % (1020483)Termination reason: Instruction limit
% 40.97/6.83 % (1020483)Termination phase: Saturation
% 40.97/6.83 % (1020483)Time elapsed: 0.161 s
% 40.97/6.83 % (1020483)Peak memory usage: 102 MB
% 40.97/6.83 % (1020483)Instructions burned: 595 (million)
% 40.97/6.83 % (1020485)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2647485730:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 40.97/6.83 % (1020474)Instruction limit reached!
% 40.97/6.83 % (1020474)------------------------------
% 40.97/6.83 % (1020474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.83 % (1020474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.83 % (1020474)CaDiCaL version: 2.1.3
% 40.97/6.83 % (1020474)Termination reason: Instruction limit
% 40.97/6.83 % (1020474)Termination phase: Saturation
% 40.97/6.83 % (1020474)Time elapsed: 0.601 s
% 40.97/6.83 % (1020474)Peak memory usage: 104 MB
% 40.97/6.83 % (1020474)Instructions burned: 908 (million)
% 40.97/6.83 % (1020487)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=2401929358:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 68.77/10.64 % (1020487)Instruction limit reached!
% 68.77/10.64 % (1020487)------------------------------
% 68.77/10.64 % (1020487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.64 % (1020487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.64 % (1020487)CaDiCaL version: 2.1.3
% 68.77/10.64 % (1020487)Termination reason: Instruction limit
% 68.77/10.64 % (1020487)Termination phase: Saturation
% 68.77/10.64 % (1020487)Time elapsed: 0.074 s
% 68.77/10.64 % (1020487)Peak memory usage: 93 MB
% 68.77/10.64 % (1020487)Instructions burned: 126 (million)
% 68.77/10.64 % (1020489)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4250939942:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi)
% 68.77/10.64 % (1020489)Instruction limit reached!
% 68.77/10.64 % (1020489)------------------------------
% 68.77/10.64 % (1020489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.64 % (1020489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.64 % (1020489)CaDiCaL version: 2.1.3
% 68.77/10.64 % (1020489)Termination reason: Instruction limit
% 68.77/10.64 % (1020489)Termination phase: Preprocessing 3
% 68.77/10.64 % (1020489)Time elapsed: 0.080 s
% 68.77/10.64 % (1020489)Peak memory usage: 92 MB
% 68.77/10.64 % (1020489)Instructions burned: 135 (million)
% 68.77/10.64 % (1020491)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1183402357:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 68.77/10.64 % (1020466)Instruction limit reached!
% 68.77/10.64 % (1020466)------------------------------
% 68.77/10.64 % (1020466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.64 % (1020466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.64 % (1020466)CaDiCaL version: 2.1.3
% 68.77/10.64 % (1020466)Termination reason: Instruction limit
% 68.77/10.64 % (1020466)Termination phase: Saturation
% 68.77/10.64 % (1020466)Time elapsed: 1.452 s
% 68.77/10.64 % (1020466)Peak memory usage: 211 MB
% 68.77/10.64 % (1020466)Instructions burned: 2355 (million)
% 68.77/10.64 % (1020491)Instruction limit reached!
% 68.77/10.64 % (1020491)------------------------------
% 68.77/10.64 % (1020491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.64 % (1020491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.64 % (1020491)CaDiCaL version: 2.1.3
% 68.77/10.64 % (1020491)Termination reason: Instruction limit
% 68.77/10.64 % (1020491)Termination phase: Saturation
% 68.77/10.64 % (1020491)Time elapsed: 0.092 s
% 68.77/10.64 % (1020491)Peak memory usage: 94 MB
% 68.77/10.64 % (1020491)Instructions burned: 142 (million)
% 68.77/10.64 % (1020493)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=458243199:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 68.77/10.64 % (1020494)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=1274705721:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 68.77/10.64 % (1020493)Instruction limit reached!
% 68.77/10.64 % (1020493)------------------------------
% 68.77/10.64 % (1020493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.64 % (1020493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.64 % (1020493)CaDiCaL version: 2.1.3
% 68.77/10.64 % (1020493)Termination reason: Instruction limit
% 68.77/10.64 % (1020493)Termination phase: Saturation
% 68.77/10.64 % (1020493)Time elapsed: 0.270 s
% 68.77/10.64 % (1020493)Peak memory usage: 96 MB
% 68.77/10.64 % (1020493)Instructions burned: 433 (million)
% 68.77/10.64 % (1020497)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=2490739865:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 68.77/10.64 % (1020497)Instruction limit reached!
% 68.77/10.64 % (1020497)------------------------------
% 68.77/10.64 % (1020497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.64 % (1020497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.64 % (1020497)CaDiCaL version: 2.1.3
% 68.77/10.64 % (1020497)Termination reason: Instruction limit
% 70.64/11.01 % (1020497)Termination phase: Property scanning
% 70.64/11.01 % (1020497)Time elapsed: 0.084 s
% 70.64/11.01 % (1020497)Peak memory usage: 94 MB
% 70.64/11.01 % (1020497)Instructions burned: 152 (million)
% 70.64/11.01 % (1020499)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1748852381:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 70.64/11.01 % (1020477)Instruction limit reached!
% 70.64/11.01 % (1020477)------------------------------
% 70.64/11.01 % (1020477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020477)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020477)Termination reason: Instruction limit
% 70.64/11.01 % (1020477)Termination phase: Saturation
% 70.64/11.01 % (1020477)Time elapsed: 3.255 s
% 70.64/11.01 % (1020477)Peak memory usage: 189 MB
% 70.64/11.01 % (1020477)Instructions burned: 5204 (million)
% 70.64/11.01 % (1020501)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3760022938:i=667:av=off:fsr=off_2956 on theBenchmark for (2956ds/667Mi)
% 70.64/11.01 % (1020501)Instruction limit reached!
% 70.64/11.01 % (1020501)------------------------------
% 70.64/11.01 % (1020501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020501)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020501)Termination reason: Instruction limit
% 70.64/11.01 % (1020501)Termination phase: Saturation
% 70.64/11.01 % (1020501)Time elapsed: 0.290 s
% 70.64/11.01 % (1020501)Peak memory usage: 101 MB
% 70.64/11.01 % (1020501)Instructions burned: 669 (million)
% 70.64/11.01 % (1020503)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=3942977224:s2a=on:i=185:s2at=1.8:fdi=4_2952 on theBenchmark for (2952ds/185Mi)
% 70.64/11.01 % (1020503)Instruction limit reached!
% 70.64/11.01 % (1020503)------------------------------
% 70.64/11.01 % (1020503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020503)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020503)Termination reason: Instruction limit
% 70.64/11.01 % (1020503)Termination phase: Property scanning
% 70.64/11.01 % (1020503)Time elapsed: 0.105 s
% 70.64/11.01 % (1020503)Peak memory usage: 94 MB
% 70.64/11.01 % (1020503)Instructions burned: 187 (million)
% 70.64/11.01 % (1020505)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=619440893:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 70.64/11.01 % (1020505)Instruction limit reached!
% 70.64/11.01 % (1020505)------------------------------
% 70.64/11.01 % (1020505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020505)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020505)Termination reason: Instruction limit
% 70.64/11.01 % (1020505)Termination phase: Saturation
% 70.64/11.01 % (1020505)Time elapsed: 0.117 s
% 70.64/11.01 % (1020505)Peak memory usage: 95 MB
% 70.64/11.01 % (1020505)Instructions burned: 194 (million)
% 70.64/11.01 % (1020507)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2280847017:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2947 on theBenchmark for (2947ds/4850Mi)
% 70.64/11.01 % (1020485)Instruction limit reached!
% 70.64/11.01 % (1020485)------------------------------
% 70.64/11.01 % (1020485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020485)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020485)Termination reason: Instruction limit
% 70.64/11.01 % (1020485)Termination phase: Saturation
% 70.64/11.01 % (1020485)Time elapsed: 4.226 s
% 70.64/11.01 % (1020485)Peak memory usage: 247 MB
% 70.64/11.01 % (1020485)Instructions burned: 13194 (million)
% 70.64/11.01 % (1020509)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4046365941:i=12111:sd=1:ss=included_2942 on theBenchmark for (2942ds/12111Mi)
% 70.64/11.01 % (1020494)Instruction limit reached!
% 70.64/11.01 % (1020494)------------------------------
% 70.64/11.01 % (1020494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020494)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020494)Termination reason: Instruction limit
% 70.64/11.01 % (1020494)Termination phase: Saturation
% 70.64/11.01 % (1020494)Time elapsed: 3.608 s
% 70.64/11.01 % (1020494)Peak memory usage: 216 MB
% 70.64/11.01 % (1020494)Instructions burned: 6062 (million)
% 70.64/11.01 % (1020511)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2187773858:i=319:kws=precedence:fsr=off_2940 on theBenchmark for (2940ds/319Mi)
% 70.64/11.01 % (1020511)Instruction limit reached!
% 70.64/11.01 % (1020511)------------------------------
% 70.64/11.01 % (1020511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020511)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020511)Termination reason: Instruction limit
% 70.64/11.01 % (1020511)Termination phase: Saturation
% 70.64/11.01 % (1020511)Time elapsed: 0.150 s
% 70.64/11.01 % (1020511)Peak memory usage: 97 MB
% 70.64/11.01 % (1020511)Instructions burned: 319 (million)
% 70.64/11.01 % (1020513)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1576718610:i=2064:ep=RST_2937 on theBenchmark for (2937ds/2064Mi)
% 70.64/11.01 % (1020513)Instruction limit reached!
% 70.64/11.01 % (1020513)------------------------------
% 70.64/11.01 % (1020513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020513)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020513)Termination reason: Instruction limit
% 70.64/11.01 % (1020513)Termination phase: Saturation
% 70.64/11.01 % (1020513)Time elapsed: 1.103 s
% 70.64/11.01 % (1020513)Peak memory usage: 118 MB
% 70.64/11.01 % (1020513)Instructions burned: 2065 (million)
% 70.64/11.01 % (1020515)dis-1011_128_sil=32000:random_seed=806183073:i=3706:ep=RST:av=off_2924 on theBenchmark for (2924ds/3706Mi)
% 70.64/11.01 % (1020507)Instruction limit reached!
% 70.64/11.01 % (1020507)------------------------------
% 70.64/11.01 % (1020507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020507)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020507)Termination reason: Instruction limit
% 70.64/11.01 % (1020507)Termination phase: Saturation
% 70.64/11.01 % (1020507)Time elapsed: 2.593 s
% 70.64/11.01 % (1020507)Peak memory usage: 124 MB
% 70.64/11.01 % (1020507)Instructions burned: 4851 (million)
% 70.64/11.01 % (1020517)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=721770367:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2920 on theBenchmark for (2920ds/757Mi)
% 70.64/11.01 % (1020517)Instruction limit reached!
% 70.64/11.01 % (1020517)------------------------------
% 70.64/11.01 % (1020517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020517)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020517)Termination reason: Instruction limit
% 70.64/11.01 % (1020517)Termination phase: Saturation
% 70.64/11.01 % (1020517)Time elapsed: 0.548 s
% 70.64/11.01 % (1020517)Peak memory usage: 99 MB
% 70.64/11.01 % (1020517)Instructions burned: 757 (million)
% 70.64/11.01 % (1020519)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2509631951:i=13913:ss=axioms:sgt=8_2913 on theBenchmark for (2913ds/13913Mi)
% 70.64/11.01 % (1020499)Instruction limit reached!
% 70.64/11.01 % (1020499)------------------------------
% 70.64/11.01 % (1020499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020499)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020499)Termination reason: Instruction limit
% 70.64/11.01 % (1020499)Termination phase: Saturation
% 70.64/11.01 % (1020499)Time elapsed: 6.021 s
% 70.64/11.01 % (1020499)Peak memory usage: 251 MB
% 70.64/11.01 % (1020499)Instructions burned: 14155 (million)
% 70.64/11.01 % (1020521)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2126045114:i=9925:aac=none_2910 on theBenchmark for (2910ds/9925Mi)
% 70.64/11.01 % (1020515)Instruction limit reached!
% 70.64/11.01 % (1020515)------------------------------
% 70.64/11.01 % (1020515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.64/11.01 % (1020515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.64/11.01 % (1020515)CaDiCaL version: 2.1.3
% 70.64/11.01 % (1020515)Termination reason: Instruction limit
% 70.64/11.01 % (1020515)Termination phase: Saturation
% 70.64/11.01 % (1020515)Time elapsed: 2.114 s
% 70.64/11.01 % (1020515)Peak memory usage: 128 MB
% 70.64/11.01 % (1020515)Instructions burned: 3706 (million)
% 70.64/11.01 % (1020443)First to succeed.
% 70.64/11.01 % (1020443)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1020438"
% 70.64/11.01 % (1020523)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3002273958:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2902 on theBenchmark for (2902ds/2479Mi)
% 70.64/11.01 % (1020443)Refutation found. Thanks to Tanya!
% 70.64/11.01 % SZS status Theorem for theBenchmark
% 70.64/11.01 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/11.21 % (1020443)------------------------------
% 0.15/11.21 % (1020443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/11.21 % (1020443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/11.21 % (1020443)CaDiCaL version: 2.1.3
% 0.15/11.21 % (1020443)Termination reason: Refutation
% 0.15/11.21 % (1020443)Time elapsed: 9.576 s
% 0.15/11.21 % (1020443)Peak memory usage: 292 MB
% 0.15/11.21 % (1020443)Instructions burned: 15946 (million)
% 0.15/11.21 % (1020443)------------------------------
% 0.15/11.21 % (1020443)------------------------------
% 0.15/11.21 % (1020438)Success in time 10.15 s
% 0.15/11.21 % Vampire exiting
%------------------------------------------------------------------------------