%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT290+1 : 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 : n026.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:34 AM UTC 2026
% Result : Theorem 15.53s 3.42s
% Output : Refutation 18.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 61
% Syntax : Number of formulae : 418 ( 57 unt; 38 def)
% Number of atoms : 1831 ( 129 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 2405 ( 992 ~;1223 |; 113 &)
% ( 52 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 55 ( 53 usr; 39 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 1 con; 0-3 aty)
% Number of variables : 306 ( 0 sgn 293 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k3_tarski(k10_lopclset(X0)) = k7_lopclset(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_lopclset) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k3_tarski(k10_lopclset(X0)) = k7_lopclset(X0) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
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(f39,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> k1_lopclset(X0) = a_1_0_lopclset(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_lopclset) ).
fof(f41,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v3_pre_topc(X1,X0)
<=> r2_hidden(X1,u1_pre_topc(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_pre_topc) ).
fof(f43,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( v1_pre_topc(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ( X1 = k11_lopclset(X0)
<=> ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_lopclset) ).
fof(f46,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ( v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0))
& l1_pre_topc(k11_lopclset(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_lopclset) ).
fof(f55,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f63,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f81,axiom,
! [X0] :
? [X1] : m1_subset_1(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f86,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ~ v1_xboole_0(k1_lopclset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lopclset) ).
fof(f96,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k11_lopclset(X0))
& v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_lopclset) ).
fof(f100,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& l1_pre_topc(X1) )
=> ( r2_hidden(X0,a_1_0_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& X0 = X2
& v3_pre_topc(X2,X1)
& v4_pre_topc(X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_1_0_lopclset) ).
fof(f102,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& ~ v3_realset2(X1)
& l3_lattices(X1) )
=> ( r2_hidden(X0,a_1_2_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& X0 = k5_setfam_1(k7_lopclset(X1),X2)
& r1_tarski(X2,k10_lopclset(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_1_2_lopclset) ).
fof(f122,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(f123,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> k5_setfam_1(X0,X1) = k3_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_setfam_1) ).
fof(f128,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f129,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k4_subset_1(u1_struct_0(X0),X1,k3_subset_1(u1_struct_0(X0),X1)) = k2_pre_topc(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_pre_topc) ).
fof(f132,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> r1_tarski(k10_lopclset(X0),k1_zfmisc_1(k7_lopclset(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_lopclset) ).
fof(f133,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X1,X0)
<=> v3_pre_topc(k3_subset_1(u1_struct_0(X0),X1),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_tops_1) ).
fof(f135,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f144,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X0,X1)
& r1_tarski(X2,X1) )
=> r1_tarski(k2_xboole_0(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_xboole_1) ).
fof(f145,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
=> r1_tarski(k3_tarski(X0),k3_tarski(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t95_zfmisc_1) ).
fof(f147,axiom,
! [X0] : k3_tarski(k1_zfmisc_1(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t99_zfmisc_1) ).
fof(f171,plain,
? [X0] :
( k3_tarski(k10_lopclset(X0)) != k7_lopclset(X0)
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f172,plain,
? [X0] :
( k3_tarski(k10_lopclset(X0)) != k7_lopclset(X0)
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f171]) ).
fof(f215,plain,
! [X0] :
( k1_lopclset(X0) = a_1_0_lopclset(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f216,plain,
! [X0] :
( k1_lopclset(X0) = a_1_0_lopclset(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f215]) ).
fof(f219,plain,
! [X0] :
( ! [X1] :
( ( v3_pre_topc(X1,X0)
<=> r2_hidden(X1,u1_pre_topc(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f222,plain,
! [X0] :
( ! [X1] :
( ( X1 = k11_lopclset(X0)
<=> ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) ) )
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f223,plain,
! [X0] :
( ! [X1] :
( ( X1 = k11_lopclset(X0)
<=> ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) ) )
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f222]) ).
fof(f225,plain,
! [X0] :
( ( v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0))
& l1_pre_topc(k11_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f46]) ).
fof(f226,plain,
! [X0] :
( ( v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0))
& l1_pre_topc(k11_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f225]) ).
fof(f232,plain,
! [X0,X1] :
( m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f55]) ).
fof(f243,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f63]) ).
fof(f258,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f86]) ).
fof(f259,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f258]) ).
fof(f278,plain,
! [X0] :
( ( ~ v3_struct_0(k11_lopclset(X0))
& v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f96]) ).
fof(f279,plain,
! [X0] :
( ( ~ v3_struct_0(k11_lopclset(X0))
& v1_pre_topc(k11_lopclset(X0))
& v2_pre_topc(k11_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f278]) ).
fof(f284,plain,
! [X0,X1] :
( ( r2_hidden(X0,a_1_0_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& X0 = X2
& v3_pre_topc(X2,X1)
& v4_pre_topc(X2,X1) ) )
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(ennf_transformation,[],[f100]) ).
fof(f285,plain,
! [X0,X1] :
( ( r2_hidden(X0,a_1_0_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& X0 = X2
& v3_pre_topc(X2,X1)
& v4_pre_topc(X2,X1) ) )
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(flattening,[],[f284]) ).
fof(f288,plain,
! [X0,X1] :
( ( r2_hidden(X0,a_1_2_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& X0 = k5_setfam_1(k7_lopclset(X1),X2)
& r1_tarski(X2,k10_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(ennf_transformation,[],[f102]) ).
fof(f289,plain,
! [X0,X1] :
( ( r2_hidden(X0,a_1_2_lopclset(X1))
<=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& X0 = k5_setfam_1(k7_lopclset(X1),X2)
& r1_tarski(X2,k10_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(flattening,[],[f288]) ).
fof(f306,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,[],[f122]) ).
fof(f307,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,[],[f306]) ).
fof(f308,plain,
! [X0,X1] :
( k5_setfam_1(X0,X1) = k3_tarski(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f123]) ).
fof(f313,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f128]) ).
fof(f314,plain,
! [X0] :
( ! [X1] :
( k4_subset_1(u1_struct_0(X0),X1,k3_subset_1(u1_struct_0(X0),X1)) = k2_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f129]) ).
fof(f316,plain,
! [X0] :
( r1_tarski(k10_lopclset(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f132]) ).
fof(f317,plain,
! [X0] :
( r1_tarski(k10_lopclset(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f316]) ).
fof(f318,plain,
! [X0] :
( ! [X1] :
( ( v4_pre_topc(X1,X0)
<=> v3_pre_topc(k3_subset_1(u1_struct_0(X0),X1),X0) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f133]) ).
fof(f321,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f135]) ).
fof(f322,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f321]) ).
fof(f332,plain,
! [X0,X1,X2] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(ennf_transformation,[],[f144]) ).
fof(f333,plain,
! [X0,X1,X2] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(flattening,[],[f332]) ).
fof(f334,plain,
! [X0,X1] :
( r1_tarski(k3_tarski(X0),k3_tarski(X1))
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f145]) ).
fof(f335,plain,
( k3_tarski(k10_lopclset(sK0)) != k7_lopclset(sK0)
& ~ v3_struct_0(sK0)
& v10_lattices(sK0)
& v17_lattices(sK0)
& ~ v3_realset2(sK0)
& l3_lattices(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f172]) ).
fof(f336,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(f337,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,[],[f336]) ).
fof(f338,plain,
! [X0] :
( ! [X1] :
( ( ( v3_pre_topc(X1,X0)
| ~ r2_hidden(X1,u1_pre_topc(X0)) )
& ( r2_hidden(X1,u1_pre_topc(X0))
| ~ v3_pre_topc(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f219]) ).
fof(f339,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k11_lopclset(X0)
| k7_lopclset(X0) != u1_struct_0(X1)
| u1_pre_topc(X1) != a_1_2_lopclset(X0) )
& ( ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) )
| k11_lopclset(X0) != X1 ) )
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f223]) ).
fof(f340,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k11_lopclset(X0)
| k7_lopclset(X0) != u1_struct_0(X1)
| u1_pre_topc(X1) != a_1_2_lopclset(X0) )
& ( ( u1_struct_0(X1) = k7_lopclset(X0)
& u1_pre_topc(X1) = a_1_2_lopclset(X0) )
| k11_lopclset(X0) != X1 ) )
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f339]) ).
fof(f348,plain,
! [X0] : m1_subset_1(sK8(X0),X0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X1,sK8(X0))],[f81]) ).
fof(f351,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_0_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| X0 != X2
| ~ v3_pre_topc(X2,X1)
| ~ v4_pre_topc(X2,X1) ) )
& ( ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& X0 = X2
& v3_pre_topc(X2,X1)
& v4_pre_topc(X2,X1) )
| ~ r2_hidden(X0,a_1_0_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(nnf_transformation,[],[f285]) ).
fof(f352,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_0_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| X0 != X2
| ~ v3_pre_topc(X2,X1)
| ~ v4_pre_topc(X2,X1) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& X0 = X3
& v3_pre_topc(X3,X1)
& v4_pre_topc(X3,X1) )
| ~ r2_hidden(X0,a_1_0_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(rectify,[],[f351]) ).
fof(f353,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_0_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| X0 != X2
| ~ v3_pre_topc(X2,X1)
| ~ v4_pre_topc(X2,X1) ) )
& ( ( m1_subset_1(sK11(X0,X1),k1_zfmisc_1(u1_struct_0(X1)))
& sK11(X0,X1) = X0
& v3_pre_topc(sK11(X0,X1),X1)
& v4_pre_topc(sK11(X0,X1),X1) )
| ~ r2_hidden(X0,a_1_0_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X3,sK11(X0,X1))],[f352]) ).
fof(f357,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_2_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
| k5_setfam_1(k7_lopclset(X1),X2) != X0
| ~ r1_tarski(X2,k10_lopclset(X1)) ) )
& ( ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& X0 = k5_setfam_1(k7_lopclset(X1),X2)
& r1_tarski(X2,k10_lopclset(X1)) )
| ~ r2_hidden(X0,a_1_2_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(nnf_transformation,[],[f289]) ).
fof(f358,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_2_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
| k5_setfam_1(k7_lopclset(X1),X2) != X0
| ~ r1_tarski(X2,k10_lopclset(X1)) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& k5_setfam_1(k7_lopclset(X1),X3) = X0
& r1_tarski(X3,k10_lopclset(X1)) )
| ~ r2_hidden(X0,a_1_2_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(rectify,[],[f357]) ).
fof(f359,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,a_1_2_lopclset(X1))
| ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
| k5_setfam_1(k7_lopclset(X1),X2) != X0
| ~ r1_tarski(X2,k10_lopclset(X1)) ) )
& ( ( m1_subset_1(sK13(X0,X1),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
& k5_setfam_1(k7_lopclset(X1),sK13(X0,X1)) = X0
& r1_tarski(sK13(X0,X1),k10_lopclset(X1)) )
| ~ r2_hidden(X0,a_1_2_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X3,sK13(X0,X1))],[f358]) ).
fof(f375,plain,
! [X0] :
( ! [X1] :
( ( ( v4_pre_topc(X1,X0)
| ~ v3_pre_topc(k3_subset_1(u1_struct_0(X0),X1),X0) )
& ( v3_pre_topc(k3_subset_1(u1_struct_0(X0),X1),X0)
| ~ v4_pre_topc(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f318]) ).
fof(f379,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f335]) ).
fof(f380,plain,
~ v3_realset2(sK0),
inference(cnf_transformation,[],[f335]) ).
fof(f381,plain,
v17_lattices(sK0),
inference(cnf_transformation,[],[f335]) ).
fof(f382,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f335]) ).
fof(f383,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f335]) ).
fof(f384,plain,
k3_tarski(k10_lopclset(sK0)) != k7_lopclset(sK0),
inference(cnf_transformation,[],[f335]) ).
fof(f460,plain,
! [X0,X1] :
( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) ),
inference(cnf_transformation,[],[f337]) ).
fof(f461,plain,
! [X0] :
( k1_lopclset(X0) = a_1_0_lopclset(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f216]) ).
fof(f463,plain,
! [X0,X1] :
( r2_hidden(X1,u1_pre_topc(X0))
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f338]) ).
fof(f466,plain,
! [X0,X1] :
( u1_pre_topc(X1) = a_1_2_lopclset(X0)
| k11_lopclset(X0) != X1
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f340]) ).
fof(f467,plain,
! [X0,X1] :
( k7_lopclset(X0) = u1_struct_0(X1)
| k11_lopclset(X0) != X1
| ~ v1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f340]) ).
fof(f471,plain,
! [X0] :
( l1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f477,plain,
! [X0,X1] :
( m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f232]) ).
fof(f486,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f243]) ).
fof(f502,plain,
! [X0] : m1_subset_1(sK8(X0),X0),
inference(cnf_transformation,[],[f348]) ).
fof(f510,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f259]) ).
fof(f530,plain,
! [X0] :
( v2_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f531,plain,
! [X0] :
( v1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f532,plain,
! [X0] :
( ~ v3_struct_0(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f541,plain,
! [X0,X1] :
( v4_pre_topc(sK11(X0,X1),X1)
| ~ r2_hidden(X0,a_1_0_lopclset(X1))
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f353]) ).
fof(f542,plain,
! [X0,X1] :
( v3_pre_topc(sK11(X0,X1),X1)
| ~ r2_hidden(X0,a_1_0_lopclset(X1))
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f353]) ).
fof(f543,plain,
! [X0,X1] :
( sK11(X0,X1) = X0
| ~ r2_hidden(X0,a_1_0_lopclset(X1))
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f353]) ).
fof(f544,plain,
! [X0,X1] :
( m1_subset_1(sK11(X0,X1),k1_zfmisc_1(u1_struct_0(X1)))
| ~ r2_hidden(X0,a_1_0_lopclset(X1))
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f353]) ).
fof(f550,plain,
! [X0,X1] :
( r1_tarski(sK13(X0,X1),k10_lopclset(X1))
| ~ r2_hidden(X0,a_1_2_lopclset(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f359]) ).
fof(f551,plain,
! [X0,X1] :
( k5_setfam_1(k7_lopclset(X1),sK13(X0,X1)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f359]) ).
fof(f552,plain,
! [X0,X1] :
( m1_subset_1(sK13(X0,X1),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(X1))))
| ~ r2_hidden(X0,a_1_2_lopclset(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f359]) ).
fof(f611,plain,
! [X2,X0,X1] :
( 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(cnf_transformation,[],[f307]) ).
fof(f612,plain,
! [X0,X1] :
( k5_setfam_1(X0,X1) = k3_tarski(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f308]) ).
fof(f619,plain,
! [X0] :
( u1_struct_0(X0) = k2_pre_topc(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f313]) ).
fof(f620,plain,
! [X0,X1] :
( k2_pre_topc(X0) = k4_subset_1(u1_struct_0(X0),X1,k3_subset_1(u1_struct_0(X0),X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f314]) ).
fof(f623,plain,
! [X0] :
( r1_tarski(k10_lopclset(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f317]) ).
fof(f624,plain,
! [X0,X1] :
( v3_pre_topc(k3_subset_1(u1_struct_0(X0),X1),X0)
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f375]) ).
fof(f627,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f322]) ).
fof(f638,plain,
! [X2,X0,X1] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(cnf_transformation,[],[f333]) ).
fof(f639,plain,
! [X0,X1] :
( r1_tarski(k3_tarski(X0),k3_tarski(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f334]) ).
fof(f641,plain,
! [X0] : k3_tarski(k1_zfmisc_1(X0)) = X0,
inference(cnf_transformation,[],[f147]) ).
fof(f644,plain,
! [X0] :
( k7_lopclset(X0) = u1_struct_0(k11_lopclset(X0))
| ~ v1_pre_topc(k11_lopclset(X0))
| ~ v2_pre_topc(k11_lopclset(X0))
| ~ l1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f467]) ).
fof(f645,plain,
! [X0] :
( a_1_2_lopclset(X0) = u1_pre_topc(k11_lopclset(X0))
| ~ v1_pre_topc(k11_lopclset(X0))
| ~ v2_pre_topc(k11_lopclset(X0))
| ~ l1_pre_topc(k11_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f466]) ).
fof(f656,definition,
( spl31_1
<=> l3_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl31_1])],[avatar_definition]) ).
fof(f658,plain,
( l3_lattices(sK0)
| ~ spl31_1 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f659,plain,
spl31_1,
inference(avatar_split_clause,[],[f379,f656]) ).
fof(f661,definition,
( spl31_2
<=> v3_struct_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl31_2])],[avatar_definition]) ).
fof(f663,plain,
( ~ v3_struct_0(sK0)
| spl31_2 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f664,plain,
~ spl31_2,
inference(avatar_split_clause,[],[f383,f661]) ).
fof(f666,definition,
( spl31_3
<=> v10_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl31_3])],[avatar_definition]) ).
fof(f668,plain,
( v10_lattices(sK0)
| ~ spl31_3 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f669,plain,
spl31_3,
inference(avatar_split_clause,[],[f382,f666]) ).
fof(f671,definition,
( spl31_4
<=> v17_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl31_4])],[avatar_definition]) ).
fof(f673,plain,
( v17_lattices(sK0)
| ~ spl31_4 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f674,plain,
spl31_4,
inference(avatar_split_clause,[],[f381,f671]) ).
fof(f676,definition,
( spl31_5
<=> v3_realset2(sK0) ),
introduced(definition,[new_symbols(definition,[spl31_5])],[avatar_definition]) ).
fof(f678,plain,
( ~ v3_realset2(sK0)
| spl31_5 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f679,plain,
~ spl31_5,
inference(avatar_split_clause,[],[f380,f676]) ).
fof(f705,plain,
( l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1 ),
inference(resolution,[],[f658,f471]) ).
fof(f720,plain,
( v2_pre_topc(k11_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1 ),
inference(resolution,[],[f658,f530]) ).
fof(f721,plain,
( v1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1 ),
inference(resolution,[],[f658,f531]) ).
fof(f722,plain,
( ~ v3_struct_0(k11_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1 ),
inference(resolution,[],[f658,f532]) ).
fof(f726,plain,
( ! [X0] :
( r1_tarski(sK13(X0,sK0),k10_lopclset(sK0))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1 ),
inference(resolution,[],[f658,f550]) ).
fof(f727,plain,
( ! [X0] :
( k5_setfam_1(k7_lopclset(sK0),sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1 ),
inference(resolution,[],[f658,f551]) ).
fof(f728,plain,
( ! [X0] :
( m1_subset_1(sK13(X0,sK0),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK0))))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1 ),
inference(resolution,[],[f658,f552]) ).
fof(f730,plain,
( r1_tarski(k10_lopclset(sK0),k1_zfmisc_1(k7_lopclset(sK0)))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1 ),
inference(resolution,[],[f658,f623]) ).
fof(f731,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1 ),
inference(resolution,[],[f658,f644]) ).
fof(f732,plain,
( a_1_2_lopclset(sK0) = u1_pre_topc(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1 ),
inference(resolution,[],[f658,f645]) ).
fof(f737,plain,
( a_1_2_lopclset(sK0) = u1_pre_topc(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f732,f663]) ).
fof(f738,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f731,f663]) ).
fof(f739,plain,
( r1_tarski(k10_lopclset(sK0),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f730,f663]) ).
fof(f741,plain,
( ! [X0] :
( m1_subset_1(sK13(X0,sK0),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK0))))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f728,f663]) ).
fof(f742,plain,
( ! [X0] :
( k5_setfam_1(k7_lopclset(sK0),sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f727,f663]) ).
fof(f743,plain,
( ! [X0] :
( r1_tarski(sK13(X0,sK0),k10_lopclset(sK0))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f726,f663]) ).
fof(f747,plain,
( ~ v3_struct_0(k11_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f722,f663]) ).
fof(f748,plain,
( v1_pre_topc(k11_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f721,f663]) ).
fof(f749,plain,
( v2_pre_topc(k11_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f720,f663]) ).
fof(f762,plain,
( l1_pre_topc(k11_lopclset(sK0))
| ~ v10_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2 ),
inference(forward_subsumption_resolution,[],[f705,f663]) ).
fof(f788,plain,
( a_1_2_lopclset(sK0) = u1_pre_topc(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f737,f668]) ).
fof(f789,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f738,f668]) ).
fof(f790,plain,
( r1_tarski(k10_lopclset(sK0),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f739,f668]) ).
fof(f792,plain,
( ! [X0] :
( m1_subset_1(sK13(X0,sK0),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK0))))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f741,f668]) ).
fof(f793,plain,
( ! [X0] :
( k5_setfam_1(k7_lopclset(sK0),sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f742,f668]) ).
fof(f794,plain,
( ! [X0] :
( r1_tarski(sK13(X0,sK0),k10_lopclset(sK0))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f743,f668]) ).
fof(f798,plain,
( ~ v3_struct_0(k11_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f747,f668]) ).
fof(f799,plain,
( v1_pre_topc(k11_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f748,f668]) ).
fof(f800,plain,
( v2_pre_topc(k11_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f749,f668]) ).
fof(f813,plain,
( l1_pre_topc(k11_lopclset(sK0))
| ~ v17_lattices(sK0)
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3 ),
inference(forward_subsumption_resolution,[],[f762,f668]) ).
fof(f836,plain,
( a_1_2_lopclset(sK0) = u1_pre_topc(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f788,f673]) ).
fof(f837,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f789,f673]) ).
fof(f838,plain,
( r1_tarski(k10_lopclset(sK0),k1_zfmisc_1(k7_lopclset(sK0)))
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f790,f673]) ).
fof(f840,plain,
( ! [X0] :
( m1_subset_1(sK13(X0,sK0),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK0))))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f792,f673]) ).
fof(f841,plain,
( ! [X0] :
( k5_setfam_1(k7_lopclset(sK0),sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f793,f673]) ).
fof(f842,plain,
( ! [X0] :
( r1_tarski(sK13(X0,sK0),k10_lopclset(sK0))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| v3_realset2(sK0) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f794,f673]) ).
fof(f846,plain,
( ~ v3_struct_0(k11_lopclset(sK0))
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f798,f673]) ).
fof(f847,plain,
( v1_pre_topc(k11_lopclset(sK0))
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f799,f673]) ).
fof(f848,plain,
( v2_pre_topc(k11_lopclset(sK0))
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f800,f673]) ).
fof(f858,plain,
( l1_pre_topc(k11_lopclset(sK0))
| v3_realset2(sK0)
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f813,f673]) ).
fof(f873,plain,
( a_1_2_lopclset(sK0) = u1_pre_topc(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f836,f678]) ).
fof(f874,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ v1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f837,f678]) ).
fof(f875,plain,
( r1_tarski(k10_lopclset(sK0),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f838,f678]) ).
fof(f877,plain,
( ! [X0] :
( m1_subset_1(sK13(X0,sK0),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK0))))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f840,f678]) ).
fof(f878,plain,
( ! [X0] :
( k5_setfam_1(k7_lopclset(sK0),sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f841,f678]) ).
fof(f879,plain,
( ! [X0] :
( r1_tarski(sK13(X0,sK0),k10_lopclset(sK0))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f842,f678]) ).
fof(f883,plain,
( ~ v3_struct_0(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f846,f678]) ).
fof(f884,plain,
( v1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f847,f678]) ).
fof(f885,plain,
( v2_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f848,f678]) ).
fof(f895,plain,
( l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f858,f678]) ).
fof(f899,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(backward_subsumption_resolution,[],[f874,f884]) ).
fof(f900,plain,
( a_1_2_lopclset(sK0) = u1_pre_topc(k11_lopclset(sK0))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(backward_subsumption_resolution,[],[f873,f884]) ).
fof(f902,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f899,f885]) ).
fof(f903,plain,
( a_1_2_lopclset(sK0) = u1_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f900,f885]) ).
fof(f904,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f902,f895]) ).
fof(f905,plain,
( a_1_2_lopclset(sK0) = u1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f903,f895]) ).
fof(f993,definition,
( spl31_6
<=> k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl31_6])],[avatar_definition]) ).
fof(f995,plain,
( k7_lopclset(sK0) = u1_struct_0(k11_lopclset(sK0))
| ~ spl31_6 ),
inference(avatar_component_clause,[],[f993]) ).
fof(f996,plain,
( spl31_6
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(avatar_split_clause,[],[f904,f676,f671,f666,f661,f656,f993]) ).
fof(f999,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| r2_hidden(X0,u1_pre_topc(k11_lopclset(sK0)))
| ~ v3_pre_topc(X0,k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| ~ spl31_6 ),
inference(superposition,[],[f463,f995]) ).
fof(f1010,plain,
( ! [X0] :
( m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| v3_struct_0(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| ~ spl31_6 ),
inference(superposition,[],[f544,f995]) ).
fof(f1015,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| k2_pre_topc(k11_lopclset(sK0)) = k4_subset_1(k7_lopclset(sK0),X0,k3_subset_1(k7_lopclset(sK0),X0))
| ~ l1_struct_0(k11_lopclset(sK0)) )
| ~ spl31_6 ),
inference(superposition,[],[f620,f995]) ).
fof(f1033,plain,
( ! [X0] :
( m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_6 ),
inference(forward_subsumption_resolution,[],[f1010,f883]) ).
fof(f1042,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| r2_hidden(X0,u1_pre_topc(k11_lopclset(sK0)))
| ~ v3_pre_topc(X0,k11_lopclset(sK0)) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_6 ),
inference(forward_subsumption_resolution,[],[f999,f895]) ).
fof(f1049,plain,
( ! [X0] :
( m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_6 ),
inference(forward_subsumption_resolution,[],[f1033,f895]) ).
fof(f1054,plain,
( ! [X0] :
( r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ v3_pre_topc(X0,k11_lopclset(sK0)) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_6 ),
inference(forward_demodulation,[],[f1042,f905]) ).
fof(f1176,definition,
( spl31_8
<=> k3_tarski(k10_lopclset(sK0)) = k7_lopclset(sK0) ),
introduced(definition,[new_symbols(definition,[spl31_8])],[avatar_definition]) ).
fof(f1178,plain,
( k3_tarski(k10_lopclset(sK0)) != k7_lopclset(sK0)
| spl31_8 ),
inference(avatar_component_clause,[],[f1176]) ).
fof(f1179,plain,
~ spl31_8,
inference(avatar_split_clause,[],[f384,f1176]) ).
fof(f1286,definition,
( spl31_15
<=> v3_struct_0(k11_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl31_15])],[avatar_definition]) ).
fof(f1288,plain,
( ~ v3_struct_0(k11_lopclset(sK0))
| spl31_15 ),
inference(avatar_component_clause,[],[f1286]) ).
fof(f1289,plain,
( ~ spl31_15
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(avatar_split_clause,[],[f883,f676,f671,f666,f661,f656,f1286]) ).
fof(f1312,plain,
( k1_lopclset(k11_lopclset(sK0)) = a_1_0_lopclset(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| spl31_15 ),
inference(resolution,[],[f1288,f461]) ).
fof(f1328,plain,
( ~ v1_xboole_0(k1_lopclset(k11_lopclset(sK0)))
| ~ v2_pre_topc(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0))
| spl31_15 ),
inference(resolution,[],[f1288,f510]) ).
fof(f1336,plain,
( ! [X0] :
( v4_pre_topc(sK11(X0,k11_lopclset(sK0)),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| spl31_15 ),
inference(resolution,[],[f1288,f541]) ).
fof(f1337,plain,
( ! [X0] :
( v3_pre_topc(sK11(X0,k11_lopclset(sK0)),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| spl31_15 ),
inference(resolution,[],[f1288,f542]) ).
fof(f1338,plain,
( ! [X0] :
( sK11(X0,k11_lopclset(sK0)) = X0
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| spl31_15 ),
inference(resolution,[],[f1288,f543]) ).
fof(f1370,plain,
( ! [X0] :
( sK11(X0,k11_lopclset(sK0)) = X0
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(forward_subsumption_resolution,[],[f1338,f895]) ).
fof(f1371,plain,
( ! [X0] :
( v3_pre_topc(sK11(X0,k11_lopclset(sK0)),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(forward_subsumption_resolution,[],[f1337,f895]) ).
fof(f1372,plain,
( ! [X0] :
( v4_pre_topc(sK11(X0,k11_lopclset(sK0)),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(forward_subsumption_resolution,[],[f1336,f895]) ).
fof(f1374,plain,
( ~ v1_xboole_0(k1_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(forward_subsumption_resolution,[],[f1328,f885]) ).
fof(f1380,plain,
( k1_lopclset(k11_lopclset(sK0)) = a_1_0_lopclset(k11_lopclset(sK0))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(forward_subsumption_resolution,[],[f1312,f895]) ).
fof(f1389,plain,
( ~ v1_xboole_0(k1_lopclset(k11_lopclset(sK0)))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(forward_subsumption_resolution,[],[f1374,f895]) ).
fof(f1395,plain,
( ~ v1_xboole_0(a_1_0_lopclset(k11_lopclset(sK0)))
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(forward_demodulation,[],[f1389,f1380]) ).
fof(f1585,definition,
( spl31_26
<=> ! [X0] :
( k5_setfam_1(k7_lopclset(sK0),sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_26])],[avatar_definition]) ).
fof(f1586,plain,
( ! [X0] :
( k5_setfam_1(k7_lopclset(sK0),sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_26 ),
inference(avatar_component_clause,[],[f1585]) ).
fof(f1587,plain,
( spl31_26
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(avatar_split_clause,[],[f878,f676,f671,f666,f661,f656,f1585]) ).
fof(f1590,plain,
( ! [X0] :
( k3_tarski(sK13(X0,sK0)) = X0
| ~ m1_subset_1(sK13(X0,sK0),k1_zfmisc_1(k1_zfmisc_1(k7_lopclset(sK0))))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_26 ),
inference(superposition,[],[f612,f1586]) ).
fof(f1593,plain,
( ! [X0] :
( k3_tarski(sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_26 ),
inference(forward_subsumption_resolution,[],[f1590,f877]) ).
fof(f1596,definition,
( spl31_27
<=> ! [X0] :
( k3_tarski(sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_27])],[avatar_definition]) ).
fof(f1597,plain,
( ! [X0] :
( k3_tarski(sK13(X0,sK0)) = X0
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_27 ),
inference(avatar_component_clause,[],[f1596]) ).
fof(f1598,plain,
( spl31_27
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_26 ),
inference(avatar_split_clause,[],[f1593,f1585,f676,f671,f666,f661,f656,f1596]) ).
fof(f1683,definition,
( spl31_32
<=> l1_pre_topc(k11_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl31_32])],[avatar_definition]) ).
fof(f1685,plain,
( l1_pre_topc(k11_lopclset(sK0))
| ~ spl31_32 ),
inference(avatar_component_clause,[],[f1683]) ).
fof(f1686,plain,
( spl31_32
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(avatar_split_clause,[],[f895,f676,f671,f666,f661,f656,f1683]) ).
fof(f1695,plain,
( l1_struct_0(k11_lopclset(sK0))
| ~ spl31_32 ),
inference(resolution,[],[f1685,f486]) ).
fof(f1730,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| k2_pre_topc(k11_lopclset(sK0)) = k4_subset_1(k7_lopclset(sK0),X0,k3_subset_1(k7_lopclset(sK0),X0)) )
| ~ spl31_6
| ~ spl31_32 ),
inference(backward_subsumption_resolution,[],[f1015,f1695]) ).
fof(f1761,definition,
( spl31_33
<=> r1_tarski(k10_lopclset(sK0),k1_zfmisc_1(k7_lopclset(sK0))) ),
introduced(definition,[new_symbols(definition,[spl31_33])],[avatar_definition]) ).
fof(f1763,plain,
( r1_tarski(k10_lopclset(sK0),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ spl31_33 ),
inference(avatar_component_clause,[],[f1761]) ).
fof(f1764,plain,
( spl31_33
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(avatar_split_clause,[],[f875,f676,f671,f666,f661,f656,f1761]) ).
fof(f1765,plain,
( r1_tarski(k3_tarski(k10_lopclset(sK0)),k3_tarski(k1_zfmisc_1(k7_lopclset(sK0))))
| ~ spl31_33 ),
inference(resolution,[],[f1763,f639]) ).
fof(f1771,plain,
( r1_tarski(k3_tarski(k10_lopclset(sK0)),k7_lopclset(sK0))
| ~ spl31_33 ),
inference(forward_demodulation,[],[f1765,f641]) ).
fof(f1773,definition,
( spl31_34
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| k2_pre_topc(k11_lopclset(sK0)) = k4_subset_1(k7_lopclset(sK0),X0,k3_subset_1(k7_lopclset(sK0),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_34])],[avatar_definition]) ).
fof(f1774,plain,
( ! [X0] :
( k2_pre_topc(k11_lopclset(sK0)) = k4_subset_1(k7_lopclset(sK0),X0,k3_subset_1(k7_lopclset(sK0),X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_34 ),
inference(avatar_component_clause,[],[f1773]) ).
fof(f1775,plain,
( spl31_34
| ~ spl31_6
| ~ spl31_32 ),
inference(avatar_split_clause,[],[f1730,f1683,f993,f1773]) ).
fof(f1778,plain,
( ! [X0] :
( k2_pre_topc(k11_lopclset(sK0)) = k2_xboole_0(X0,k3_subset_1(k7_lopclset(sK0),X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ m1_subset_1(k3_subset_1(k7_lopclset(sK0),X0),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_34 ),
inference(superposition,[],[f611,f1774]) ).
fof(f1781,plain,
( ! [X0] :
( k2_pre_topc(k11_lopclset(sK0)) = k2_xboole_0(X0,k3_subset_1(k7_lopclset(sK0),X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ m1_subset_1(k3_subset_1(k7_lopclset(sK0),X0),k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_34 ),
inference(duplicate_literal_removal,[],[f1778]) ).
fof(f1783,plain,
( ! [X0] :
( k2_pre_topc(k11_lopclset(sK0)) = k2_xboole_0(X0,k3_subset_1(k7_lopclset(sK0),X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_34 ),
inference(forward_subsumption_resolution,[],[f1781,f477]) ).
fof(f1870,definition,
( spl31_40
<=> ! [X0] :
( r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ v3_pre_topc(X0,k11_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_40])],[avatar_definition]) ).
fof(f1871,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ v3_pre_topc(X0,k11_lopclset(sK0)) )
| ~ spl31_40 ),
inference(avatar_component_clause,[],[f1870]) ).
fof(f1872,plain,
( spl31_40
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_6 ),
inference(avatar_split_clause,[],[f1054,f993,f676,f671,f666,f661,f656,f1870]) ).
fof(f1880,plain,
( ! [X0] :
( r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0))
| ~ v3_pre_topc(k3_subset_1(k7_lopclset(sK0),X0),k11_lopclset(sK0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_40 ),
inference(resolution,[],[f1871,f477]) ).
fof(f2059,definition,
( spl31_44
<=> r1_tarski(k3_tarski(k10_lopclset(sK0)),k7_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl31_44])],[avatar_definition]) ).
fof(f2061,plain,
( r1_tarski(k3_tarski(k10_lopclset(sK0)),k7_lopclset(sK0))
| ~ spl31_44 ),
inference(avatar_component_clause,[],[f2059]) ).
fof(f2062,plain,
( spl31_44
| ~ spl31_33 ),
inference(avatar_split_clause,[],[f1771,f1761,f2059]) ).
fof(f2176,plain,
( k3_tarski(k10_lopclset(sK0)) = k7_lopclset(sK0)
| ~ r1_tarski(k7_lopclset(sK0),k3_tarski(k10_lopclset(sK0)))
| ~ spl31_44 ),
inference(resolution,[],[f2061,f460]) ).
fof(f2177,plain,
( ~ r1_tarski(k7_lopclset(sK0),k3_tarski(k10_lopclset(sK0)))
| spl31_8
| ~ spl31_44 ),
inference(forward_subsumption_resolution,[],[f2176,f1178]) ).
fof(f2180,definition,
( spl31_57
<=> r1_tarski(k7_lopclset(sK0),k3_tarski(k10_lopclset(sK0))) ),
introduced(definition,[new_symbols(definition,[spl31_57])],[avatar_definition]) ).
fof(f2182,plain,
( ~ r1_tarski(k7_lopclset(sK0),k3_tarski(k10_lopclset(sK0)))
| spl31_57 ),
inference(avatar_component_clause,[],[f2180]) ).
fof(f2183,plain,
( ~ spl31_57
| spl31_8
| ~ spl31_44 ),
inference(avatar_split_clause,[],[f2177,f2059,f1176,f2180]) ).
fof(f2581,definition,
( spl31_75
<=> ! [X0] :
( k2_pre_topc(k11_lopclset(sK0)) = k2_xboole_0(X0,k3_subset_1(k7_lopclset(sK0),X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_75])],[avatar_definition]) ).
fof(f2582,plain,
( ! [X0] :
( k2_pre_topc(k11_lopclset(sK0)) = k2_xboole_0(X0,k3_subset_1(k7_lopclset(sK0),X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_75 ),
inference(avatar_component_clause,[],[f2581]) ).
fof(f2583,plain,
( spl31_75
| ~ spl31_34 ),
inference(avatar_split_clause,[],[f1783,f1773,f2581]) ).
fof(f2602,plain,
( ! [X0,X1] :
( r1_tarski(k2_pre_topc(k11_lopclset(sK0)),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(k3_subset_1(k7_lopclset(sK0),X0),X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_75 ),
inference(superposition,[],[f638,f2582]) ).
fof(f2652,definition,
( spl31_81
<=> ! [X0] :
( r1_tarski(sK13(X0,sK0),k10_lopclset(sK0))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_81])],[avatar_definition]) ).
fof(f2653,plain,
( ! [X0] :
( r1_tarski(sK13(X0,sK0),k10_lopclset(sK0))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_81 ),
inference(avatar_component_clause,[],[f2652]) ).
fof(f2654,plain,
( spl31_81
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5 ),
inference(avatar_split_clause,[],[f879,f676,f671,f666,f661,f656,f2652]) ).
fof(f2656,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| r1_tarski(k3_tarski(sK13(X0,sK0)),k3_tarski(k10_lopclset(sK0))) )
| ~ spl31_81 ),
inference(resolution,[],[f2653,f639]) ).
fof(f2864,definition,
( spl31_91
<=> ! [X0] :
( m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_91])],[avatar_definition]) ).
fof(f2865,plain,
( ! [X0] :
( m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_91 ),
inference(avatar_component_clause,[],[f2864]) ).
fof(f2866,plain,
( spl31_91
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_6 ),
inference(avatar_split_clause,[],[f1049,f993,f676,f671,f666,f661,f656,f2864]) ).
fof(f2868,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| r2_hidden(sK11(X0,k11_lopclset(sK0)),a_1_2_lopclset(sK0))
| ~ v3_pre_topc(sK11(X0,k11_lopclset(sK0)),k11_lopclset(sK0)) )
| ~ spl31_40
| ~ spl31_91 ),
inference(resolution,[],[f2865,f1871]) ).
fof(f2913,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| v3_struct_0(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| ~ spl31_91 ),
inference(superposition,[],[f2865,f543]) ).
fof(f2914,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| v3_struct_0(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| ~ spl31_91 ),
inference(duplicate_literal_removal,[],[f2913]) ).
fof(f2915,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| spl31_15
| ~ spl31_91 ),
inference(forward_subsumption_resolution,[],[f2914,f1288]) ).
fof(f2931,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| r2_hidden(sK11(X0,k11_lopclset(sK0)),a_1_2_lopclset(sK0)) )
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15
| ~ spl31_40
| ~ spl31_91 ),
inference(forward_subsumption_resolution,[],[f2868,f1371]) ).
fof(f2933,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| spl31_15
| ~ spl31_32
| ~ spl31_91 ),
inference(forward_subsumption_resolution,[],[f2915,f1685]) ).
fof(f2948,definition,
( spl31_92
<=> ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| r2_hidden(sK11(X0,k11_lopclset(sK0)),a_1_2_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_92])],[avatar_definition]) ).
fof(f2949,plain,
( ! [X0] :
( r2_hidden(sK11(X0,k11_lopclset(sK0)),a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_92 ),
inference(avatar_component_clause,[],[f2948]) ).
fof(f2950,plain,
( spl31_92
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15
| ~ spl31_40
| ~ spl31_91 ),
inference(avatar_split_clause,[],[f2931,f2864,f1870,f1286,f676,f671,f666,f661,f656,f2948]) ).
fof(f2962,plain,
( ! [X0] :
( r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| v3_struct_0(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| ~ spl31_92 ),
inference(superposition,[],[f2949,f543]) ).
fof(f2963,plain,
( ! [X0] :
( r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| v3_struct_0(k11_lopclset(sK0))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| ~ spl31_92 ),
inference(duplicate_literal_removal,[],[f2962]) ).
fof(f2964,plain,
( ! [X0] :
( r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| spl31_15
| ~ spl31_92 ),
inference(forward_subsumption_resolution,[],[f2963,f1288]) ).
fof(f2969,plain,
( ! [X0] :
( r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| spl31_15
| ~ spl31_32
| ~ spl31_92 ),
inference(forward_subsumption_resolution,[],[f2964,f1685]) ).
fof(f3091,definition,
( spl31_97
<=> ! [X0] :
( sK11(X0,k11_lopclset(sK0)) = X0
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_97])],[avatar_definition]) ).
fof(f3092,plain,
( ! [X0] :
( sK11(X0,k11_lopclset(sK0)) = X0
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_97 ),
inference(avatar_component_clause,[],[f3091]) ).
fof(f3093,plain,
( spl31_97
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(avatar_split_clause,[],[f1370,f1286,f676,f671,f666,f661,f656,f3091]) ).
fof(f3462,definition,
( spl31_119
<=> l1_struct_0(k11_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl31_119])],[avatar_definition]) ).
fof(f3464,plain,
( l1_struct_0(k11_lopclset(sK0))
| ~ spl31_119 ),
inference(avatar_component_clause,[],[f3462]) ).
fof(f3465,plain,
( spl31_119
| ~ spl31_32 ),
inference(avatar_split_clause,[],[f1695,f1683,f3462]) ).
fof(f3471,plain,
( u1_struct_0(k11_lopclset(sK0)) = k2_pre_topc(k11_lopclset(sK0))
| ~ spl31_119 ),
inference(resolution,[],[f3464,f619]) ).
fof(f3475,plain,
( k7_lopclset(sK0) = k2_pre_topc(k11_lopclset(sK0))
| ~ spl31_6
| ~ spl31_119 ),
inference(forward_demodulation,[],[f3471,f995]) ).
fof(f3483,definition,
( spl31_120
<=> k7_lopclset(sK0) = k2_pre_topc(k11_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl31_120])],[avatar_definition]) ).
fof(f3485,plain,
( k7_lopclset(sK0) = k2_pre_topc(k11_lopclset(sK0))
| ~ spl31_120 ),
inference(avatar_component_clause,[],[f3483]) ).
fof(f3486,plain,
( spl31_120
| ~ spl31_6
| ~ spl31_119 ),
inference(avatar_split_clause,[],[f3475,f3462,f993,f3483]) ).
fof(f4540,definition,
( spl31_181
<=> ! [X0,X1] :
( r1_tarski(k2_pre_topc(k11_lopclset(sK0)),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(k3_subset_1(k7_lopclset(sK0),X0),X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_181])],[avatar_definition]) ).
fof(f4541,plain,
( ! [X0,X1] :
( r1_tarski(k2_pre_topc(k11_lopclset(sK0)),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(k3_subset_1(k7_lopclset(sK0),X0),X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_181 ),
inference(avatar_component_clause,[],[f4540]) ).
fof(f4542,plain,
( spl31_181
| ~ spl31_75 ),
inference(avatar_split_clause,[],[f2602,f2581,f4540]) ).
fof(f4543,plain,
( ! [X0,X1] :
( r1_tarski(k7_lopclset(sK0),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(k3_subset_1(k7_lopclset(sK0),X0),X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_120
| ~ spl31_181 ),
inference(forward_demodulation,[],[f4541,f3485]) ).
fof(f4751,definition,
( spl31_186
<=> ! [X0] :
( r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_186])],[avatar_definition]) ).
fof(f4752,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_186 ),
inference(avatar_component_clause,[],[f4751]) ).
fof(f4753,plain,
( spl31_186
| spl31_15
| ~ spl31_32
| ~ spl31_92 ),
inference(avatar_split_clause,[],[f2969,f2948,f1683,f1286,f4751]) ).
fof(f5585,definition,
( spl31_224
<=> v1_xboole_0(a_1_0_lopclset(k11_lopclset(sK0))) ),
introduced(definition,[new_symbols(definition,[spl31_224])],[avatar_definition]) ).
fof(f5587,plain,
( ~ v1_xboole_0(a_1_0_lopclset(k11_lopclset(sK0)))
| spl31_224 ),
inference(avatar_component_clause,[],[f5585]) ).
fof(f5588,plain,
( ~ spl31_224
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(avatar_split_clause,[],[f1395,f1286,f676,f671,f666,f661,f656,f5585]) ).
fof(f5611,plain,
( ! [X0] :
( r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ m1_subset_1(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| spl31_224 ),
inference(resolution,[],[f5587,f627]) ).
fof(f7419,definition,
( spl31_305
<=> ! [X0] :
( v4_pre_topc(sK11(X0,k11_lopclset(sK0)),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_305])],[avatar_definition]) ).
fof(f7420,plain,
( ! [X0] :
( v4_pre_topc(sK11(X0,k11_lopclset(sK0)),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_305 ),
inference(avatar_component_clause,[],[f7419]) ).
fof(f7421,plain,
( spl31_305
| ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15 ),
inference(avatar_split_clause,[],[f1372,f1286,f676,f671,f666,f661,f656,f7419]) ).
fof(f7422,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| v3_pre_topc(k3_subset_1(u1_struct_0(k11_lopclset(sK0)),sK11(X0,k11_lopclset(sK0))),k11_lopclset(sK0))
| ~ m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(u1_struct_0(k11_lopclset(sK0))))
| ~ l1_pre_topc(k11_lopclset(sK0)) )
| ~ spl31_305 ),
inference(resolution,[],[f7420,f624]) ).
fof(f7432,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| v3_pre_topc(k3_subset_1(u1_struct_0(k11_lopclset(sK0)),sK11(X0,k11_lopclset(sK0))),k11_lopclset(sK0))
| ~ m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(u1_struct_0(k11_lopclset(sK0)))) )
| ~ spl31_32
| ~ spl31_305 ),
inference(forward_subsumption_resolution,[],[f7422,f1685]) ).
fof(f7435,plain,
( ! [X0] :
( v3_pre_topc(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(u1_struct_0(k11_lopclset(sK0)))) )
| ~ spl31_6
| ~ spl31_32
| ~ spl31_305 ),
inference(forward_demodulation,[],[f7432,f995]) ).
fof(f7437,plain,
( ! [X0] :
( ~ m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(k7_lopclset(sK0)))
| v3_pre_topc(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_6
| ~ spl31_32
| ~ spl31_305 ),
inference(forward_demodulation,[],[f7435,f995]) ).
fof(f7439,plain,
( ! [X0] :
( v3_pre_topc(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_6
| ~ spl31_32
| ~ spl31_91
| ~ spl31_305 ),
inference(forward_subsumption_resolution,[],[f7437,f2865]) ).
fof(f7586,definition,
( spl31_313
<=> ! [X0] :
( r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0))
| ~ v3_pre_topc(k3_subset_1(k7_lopclset(sK0),X0),k11_lopclset(sK0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_313])],[avatar_definition]) ).
fof(f7587,plain,
( ! [X0] :
( ~ v3_pre_topc(k3_subset_1(k7_lopclset(sK0),X0),k11_lopclset(sK0))
| r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_313 ),
inference(avatar_component_clause,[],[f7586]) ).
fof(f7588,plain,
( spl31_313
| ~ spl31_40 ),
inference(avatar_split_clause,[],[f1880,f1870,f7586]) ).
fof(f8032,definition,
( spl31_333
<=> ! [X0] :
( v3_pre_topc(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_333])],[avatar_definition]) ).
fof(f8033,plain,
( ! [X0] :
( v3_pre_topc(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),k11_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_333 ),
inference(avatar_component_clause,[],[f8032]) ).
fof(f8034,plain,
( spl31_333
| ~ spl31_6
| ~ spl31_32
| ~ spl31_91
| ~ spl31_305 ),
inference(avatar_split_clause,[],[f7439,f7419,f2864,f1683,f993,f8032]) ).
fof(f8035,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| r2_hidden(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),a_1_2_lopclset(sK0))
| ~ m1_subset_1(sK11(X0,k11_lopclset(sK0)),k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_313
| ~ spl31_333 ),
inference(resolution,[],[f8033,f7587]) ).
fof(f8050,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| r2_hidden(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),a_1_2_lopclset(sK0)) )
| ~ spl31_91
| ~ spl31_313
| ~ spl31_333 ),
inference(forward_subsumption_resolution,[],[f8035,f2865]) ).
fof(f8061,definition,
( spl31_334
<=> ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| r2_hidden(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),a_1_2_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_334])],[avatar_definition]) ).
fof(f8062,plain,
( ! [X0] :
( r2_hidden(k3_subset_1(k7_lopclset(sK0),sK11(X0,k11_lopclset(sK0))),a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_334 ),
inference(avatar_component_clause,[],[f8061]) ).
fof(f8063,plain,
( spl31_334
| ~ spl31_91
| ~ spl31_313
| ~ spl31_333 ),
inference(avatar_split_clause,[],[f8050,f8032,f7586,f2864,f8061]) ).
fof(f8078,plain,
( ! [X0] :
( r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_97
| ~ spl31_334 ),
inference(superposition,[],[f8062,f3092]) ).
fof(f8081,plain,
( ! [X0] :
( r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_97
| ~ spl31_334 ),
inference(duplicate_literal_removal,[],[f8078]) ).
fof(f8693,definition,
( spl31_361
<=> ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_361])],[avatar_definition]) ).
fof(f8694,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_361 ),
inference(avatar_component_clause,[],[f8693]) ).
fof(f8695,plain,
( spl31_361
| spl31_15
| ~ spl31_32
| ~ spl31_91 ),
inference(avatar_split_clause,[],[f2933,f2864,f1683,f1286,f8693]) ).
fof(f10074,definition,
( spl31_414
<=> ! [X0] :
( r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ m1_subset_1(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_414])],[avatar_definition]) ).
fof(f10075,plain,
( ! [X0] :
( ~ m1_subset_1(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_414 ),
inference(avatar_component_clause,[],[f10074]) ).
fof(f10076,plain,
( spl31_414
| spl31_224 ),
inference(avatar_split_clause,[],[f5611,f5585,f10074]) ).
fof(f10082,plain,
( r2_hidden(sK8(a_1_0_lopclset(k11_lopclset(sK0))),a_1_0_lopclset(k11_lopclset(sK0)))
| ~ spl31_414 ),
inference(resolution,[],[f10075,f502]) ).
fof(f11489,definition,
( spl31_458
<=> ! [X0] :
( r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_458])],[avatar_definition]) ).
fof(f11490,plain,
( ! [X0] :
( r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_458 ),
inference(avatar_component_clause,[],[f11489]) ).
fof(f11491,plain,
( spl31_458
| ~ spl31_97
| ~ spl31_334 ),
inference(avatar_split_clause,[],[f8081,f8061,f3091,f11489]) ).
fof(f11567,definition,
( spl31_460
<=> ! [X0] :
( ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| r1_tarski(k3_tarski(sK13(X0,sK0)),k3_tarski(k10_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_460])],[avatar_definition]) ).
fof(f11568,plain,
( ! [X0] :
( r1_tarski(k3_tarski(sK13(X0,sK0)),k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_460 ),
inference(avatar_component_clause,[],[f11567]) ).
fof(f11569,plain,
( spl31_460
| ~ spl31_81 ),
inference(avatar_split_clause,[],[f2656,f2652,f11567]) ).
fof(f11576,plain,
( ! [X0] :
( r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_27
| ~ spl31_460 ),
inference(superposition,[],[f11568,f1597]) ).
fof(f11582,plain,
( ! [X0] :
( r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_27
| ~ spl31_460 ),
inference(duplicate_literal_removal,[],[f11576]) ).
fof(f11693,definition,
( spl31_464
<=> ! [X0] :
( r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_464])],[avatar_definition]) ).
fof(f11694,plain,
( ! [X0] :
( r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_464 ),
inference(avatar_component_clause,[],[f11693]) ).
fof(f11695,plain,
( spl31_464
| ~ spl31_27
| ~ spl31_460 ),
inference(avatar_split_clause,[],[f11582,f11567,f1596,f11693]) ).
fof(f15764,definition,
( spl31_580
<=> ! [X0,X1] :
( r1_tarski(k7_lopclset(sK0),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(k3_subset_1(k7_lopclset(sK0),X0),X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_580])],[avatar_definition]) ).
fof(f15765,plain,
( ! [X0,X1] :
( ~ r1_tarski(k3_subset_1(k7_lopclset(sK0),X0),X1)
| ~ r1_tarski(X0,X1)
| r1_tarski(k7_lopclset(sK0),X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0))) )
| ~ spl31_580 ),
inference(avatar_component_clause,[],[f15764]) ).
fof(f15766,plain,
( spl31_580
| ~ spl31_120
| ~ spl31_181 ),
inference(avatar_split_clause,[],[f4543,f4540,f3483,f15764]) ).
fof(f15773,plain,
( ! [X0] :
( ~ r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| r1_tarski(k7_lopclset(sK0),k3_tarski(k10_lopclset(sK0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0)) )
| ~ spl31_464
| ~ spl31_580 ),
inference(resolution,[],[f15765,f11694]) ).
fof(f15793,plain,
( ! [X0] :
( ~ r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0)) )
| spl31_57
| ~ spl31_464
| ~ spl31_580 ),
inference(forward_subsumption_resolution,[],[f15773,f2182]) ).
fof(f15795,definition,
( spl31_581
<=> ! [X0] :
( ~ r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl31_581])],[avatar_definition]) ).
fof(f15796,plain,
( ! [X0] :
( ~ r2_hidden(k3_subset_1(k7_lopclset(sK0),X0),a_1_2_lopclset(sK0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r1_tarski(X0,k3_tarski(k10_lopclset(sK0))) )
| ~ spl31_581 ),
inference(avatar_component_clause,[],[f15795]) ).
fof(f15797,plain,
( spl31_581
| spl31_57
| ~ spl31_464
| ~ spl31_580 ),
inference(avatar_split_clause,[],[f15793,f15764,f11693,f2180,f15795]) ).
fof(f15798,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k7_lopclset(sK0)))
| ~ r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_458
| ~ spl31_581 ),
inference(resolution,[],[f15796,f11490]) ).
fof(f15833,plain,
( ! [X0] :
( ~ r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_361
| ~ spl31_458
| ~ spl31_581 ),
inference(forward_subsumption_resolution,[],[f15798,f8694]) ).
fof(f15841,definition,
( spl31_582
<=> ! [X0] :
( ~ r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl31_582])],[avatar_definition]) ).
fof(f15842,plain,
( ! [X0] :
( ~ r1_tarski(X0,k3_tarski(k10_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0))) )
| ~ spl31_582 ),
inference(avatar_component_clause,[],[f15841]) ).
fof(f15843,plain,
( spl31_582
| ~ spl31_361
| ~ spl31_458
| ~ spl31_581 ),
inference(avatar_split_clause,[],[f15833,f15795,f11489,f8693,f15841]) ).
fof(f15844,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ r2_hidden(X0,a_1_2_lopclset(sK0)) )
| ~ spl31_464
| ~ spl31_582 ),
inference(resolution,[],[f15842,f11694]) ).
fof(f15851,plain,
( ! [X0] : ~ r2_hidden(X0,a_1_0_lopclset(k11_lopclset(sK0)))
| ~ spl31_186
| ~ spl31_464
| ~ spl31_582 ),
inference(forward_subsumption_resolution,[],[f15844,f4752]) ).
fof(f15885,plain,
( $false
| ~ spl31_186
| ~ spl31_414
| ~ spl31_464
| ~ spl31_582 ),
inference(backward_subsumption_resolution,[],[f10082,f15851]) ).
fof(f15894,plain,
( ~ spl31_186
| ~ spl31_414
| ~ spl31_464
| ~ spl31_582 ),
inference(avatar_contradiction_clause,[],[f15885]) ).
cnf(s1,plain,
spl31_1,
inference(sat_conversion,[],[f659]) ).
cnf(s2,plain,
~ spl31_2,
inference(sat_conversion,[],[f664]) ).
cnf(s3,plain,
spl31_3,
inference(sat_conversion,[],[f669]) ).
cnf(s4,plain,
spl31_4,
inference(sat_conversion,[],[f674]) ).
cnf(s5,plain,
~ spl31_5,
inference(sat_conversion,[],[f679]) ).
cnf(s6,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_6 ),
inference(sat_conversion,[],[f996]) ).
cnf(s8,plain,
~ spl31_8,
inference(sat_conversion,[],[f1179]) ).
cnf(s15,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_15 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s26,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_26 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s27,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_26
| spl31_27 ),
inference(sat_conversion,[],[f1598]) ).
cnf(s32,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_32 ),
inference(sat_conversion,[],[f1686]) ).
cnf(s33,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_33 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s34,plain,
( ~ spl31_6
| ~ spl31_32
| spl31_34 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s40,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_6
| spl31_40 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s44,plain,
( ~ spl31_33
| spl31_44 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s56,plain,
( spl31_8
| ~ spl31_44
| ~ spl31_57 ),
inference(sat_conversion,[],[f2183]) ).
cnf(s74,plain,
( ~ spl31_34
| spl31_75 ),
inference(sat_conversion,[],[f2583]) ).
cnf(s80,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_81 ),
inference(sat_conversion,[],[f2654]) ).
cnf(s90,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| ~ spl31_6
| spl31_91 ),
inference(sat_conversion,[],[f2866]) ).
cnf(s91,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15
| ~ spl31_40
| ~ spl31_91
| spl31_92 ),
inference(sat_conversion,[],[f2950]) ).
cnf(s96,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15
| spl31_97 ),
inference(sat_conversion,[],[f3093]) ).
cnf(s114,plain,
( ~ spl31_32
| spl31_119 ),
inference(sat_conversion,[],[f3465]) ).
cnf(s115,plain,
( ~ spl31_6
| ~ spl31_119
| spl31_120 ),
inference(sat_conversion,[],[f3486]) ).
cnf(s171,plain,
( ~ spl31_75
| spl31_181 ),
inference(sat_conversion,[],[f4542]) ).
cnf(s176,plain,
( spl31_15
| ~ spl31_32
| ~ spl31_92
| spl31_186 ),
inference(sat_conversion,[],[f4753]) ).
cnf(s213,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15
| ~ spl31_224 ),
inference(sat_conversion,[],[f5588]) ).
cnf(s290,plain,
( ~ spl31_1
| spl31_2
| ~ spl31_3
| ~ spl31_4
| spl31_5
| spl31_15
| spl31_305 ),
inference(sat_conversion,[],[f7421]) ).
cnf(s297,plain,
( ~ spl31_40
| spl31_313 ),
inference(sat_conversion,[],[f7588]) ).
cnf(s317,plain,
( ~ spl31_6
| ~ spl31_32
| ~ spl31_91
| ~ spl31_305
| spl31_333 ),
inference(sat_conversion,[],[f8034]) ).
cnf(s318,plain,
( ~ spl31_91
| ~ spl31_313
| ~ spl31_333
| spl31_334 ),
inference(sat_conversion,[],[f8063]) ).
cnf(s343,plain,
( spl31_15
| ~ spl31_32
| ~ spl31_91
| spl31_361 ),
inference(sat_conversion,[],[f8695]) ).
cnf(s422,plain,
( spl31_224
| spl31_414 ),
inference(sat_conversion,[],[f10076]) ).
cnf(s487,plain,
( ~ spl31_97
| ~ spl31_334
| spl31_458 ),
inference(sat_conversion,[],[f11491]) ).
cnf(s489,plain,
( ~ spl31_81
| spl31_460 ),
inference(sat_conversion,[],[f11569]) ).
cnf(s493,plain,
( ~ spl31_27
| ~ spl31_460
| spl31_464 ),
inference(sat_conversion,[],[f11695]) ).
cnf(s644,plain,
( ~ spl31_120
| ~ spl31_181
| spl31_580 ),
inference(sat_conversion,[],[f15766]) ).
cnf(s645,plain,
( spl31_57
| ~ spl31_464
| ~ spl31_580
| spl31_581 ),
inference(sat_conversion,[],[f15797]) ).
cnf(s646,plain,
( ~ spl31_361
| ~ spl31_458
| ~ spl31_581
| spl31_582 ),
inference(sat_conversion,[],[f15843]) ).
cnf(s647,plain,
( ~ spl31_186
| ~ spl31_414
| ~ spl31_464
| ~ spl31_582 ),
inference(sat_conversion,[],[f15894]) ).
cnf(s660,plain,
spl31_81,
inference(rat,[],[s80,s2,s5,s4,s3,s1]) ).
cnf(s672,plain,
spl31_33,
inference(rat,[],[s33,s2,s5,s4,s3,s1]) ).
cnf(s673,plain,
spl31_32,
inference(rat,[],[s32,s2,s5,s4,s3,s1]) ).
cnf(s676,plain,
spl31_26,
inference(rat,[],[s26,s2,s5,s4,s3,s1]) ).
cnf(s683,plain,
~ spl31_15,
inference(rat,[],[s15,s2,s5,s4,s3,s1]) ).
cnf(s689,plain,
spl31_6,
inference(rat,[],[s6,s2,s5,s4,s3,s1]) ).
cnf(s700,plain,
spl31_460,
inference(rat,[],[s489,s660]) ).
cnf(s709,plain,
spl31_44,
inference(rat,[],[s44,s672]) ).
cnf(s710,plain,
spl31_119,
inference(rat,[],[s114,s673]) ).
cnf(s717,plain,
spl31_27,
inference(rat,[],[s27,s1,s2,s5,s4,s3,s676]) ).
cnf(s741,plain,
spl31_305,
inference(rat,[],[s290,s1,s2,s5,s4,s3,s683]) ).
cnf(s742,plain,
~ spl31_224,
inference(rat,[],[s213,s1,s2,s5,s4,s3,s683]) ).
cnf(s745,plain,
spl31_97,
inference(rat,[],[s96,s1,s2,s5,s4,s3,s683]) ).
cnf(s754,plain,
spl31_34,
inference(rat,[],[s34,s673,s689]) ).
cnf(s762,plain,
spl31_91,
inference(rat,[],[s90,s1,s2,s5,s4,s3,s689]) ).
cnf(s770,plain,
spl31_40,
inference(rat,[],[s40,s1,s2,s5,s4,s3,s689]) ).
cnf(s788,plain,
~ spl31_57,
inference(rat,[],[s56,s8,s709]) ).
cnf(s789,plain,
spl31_120,
inference(rat,[],[s115,s689,s710]) ).
cnf(s805,plain,
spl31_464,
inference(rat,[],[s493,s700,s717]) ).
cnf(s831,plain,
spl31_414,
inference(rat,[],[s422,s742]) ).
cnf(s861,plain,
spl31_75,
inference(rat,[],[s74,s754]) ).
cnf(s880,plain,
spl31_361,
inference(rat,[],[s343,s683,s673,s762]) ).
cnf(s881,plain,
spl31_333,
inference(rat,[],[s317,s689,s741,s673,s762]) ).
cnf(s908,plain,
spl31_313,
inference(rat,[],[s297,s770]) ).
cnf(s910,plain,
spl31_92,
inference(rat,[],[s91,s762,s683,s1,s2,s5,s4,s3,s770]) ).
cnf(s996,plain,
spl31_181,
inference(rat,[],[s171,s861]) ).
cnf(s1027,plain,
spl31_334,
inference(rat,[],[s318,s881,s762,s908]) ).
cnf(s1029,plain,
spl31_186,
inference(rat,[],[s176,s683,s673,s910]) ).
cnf(s1066,plain,
spl31_580,
inference(rat,[],[s644,s789,s996]) ).
cnf(s1089,plain,
spl31_458,
inference(rat,[],[s487,s745,s1027]) ).
cnf(s1090,plain,
~ spl31_582,
inference(rat,[],[s647,s831,s805,s1029]) ).
cnf(s1107,plain,
spl31_581,
inference(rat,[],[s645,s805,s788,s1066]) ).
cnf(s1115,plain,
$false,
inference(rat,[],[s646,s1090,s880,s1107,s1089]) ).
fof(f15908,plain,
$false,
inference(avatar_sat_refutation,[],[s1115]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT290+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 14:17:12 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/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
% 12.57/2.75 % (2882848)Detected formulas, will run a generic FOF schedule.
% 12.57/2.75 % (2882858)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2396995866:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.57/2.75 % (2882855)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=1025811666:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.57/2.75 % (2882856)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=286423280:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.57/2.75 % (2882853)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=112173307:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.57/2.75 % (2882854)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=3379964135:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.57/2.75 % (2882856)Refutation not found, incomplete strategy
% 12.57/2.75 % (2882856)------------------------------
% 12.57/2.75 % (2882856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.75 % (2882856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.75 % (2882856)CaDiCaL version: 2.1.3
% 12.57/2.75 % (2882856)Termination reason: Refutation not found, incomplete strategy
% 12.57/2.75 % (2882856)Time elapsed: 0.002 s
% 12.57/2.75 % (2882856)Peak memory usage: 88 MB
% 12.57/2.75 % (2882856)Instructions burned: 1 (million)
% 12.57/2.75 % (2882859)dis-21_1_sil=8000:lcm=predicate:random_seed=4180814933:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.57/2.75 % (2882858)Instruction limit reached!
% 12.57/2.75 % (2882858)------------------------------
% 12.57/2.75 % (2882858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.75 % (2882858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.75 % (2882858)CaDiCaL version: 2.1.3
% 12.57/2.75 % (2882858)Termination reason: Instruction limit
% 12.57/2.75 % (2882858)Termination phase: Saturation
% 12.57/2.75 % (2882858)Time elapsed: 0.054 s
% 12.57/2.75 % (2882858)Peak memory usage: 90 MB
% 12.57/2.75 % (2882858)Instructions burned: 140 (million)
% 12.57/2.75 % (2882857)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1659642181:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.57/2.75 % (2882857)Instruction limit reached!
% 12.57/2.75 % (2882857)------------------------------
% 12.57/2.75 % (2882857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.75 % (2882857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.75 % (2882857)CaDiCaL version: 2.1.3
% 12.57/2.75 % (2882857)Termination reason: Instruction limit
% 12.57/2.75 % (2882857)Termination phase: Saturation
% 12.57/2.75 % (2882857)Time elapsed: 0.067 s
% 12.57/2.75 % (2882857)Peak memory usage: 89 MB
% 12.57/2.75 % (2882857)Instructions burned: 120 (million)
% 12.57/2.75 % (2882859)Instruction limit reached!
% 12.57/2.75 % (2882859)------------------------------
% 12.57/2.75 % (2882859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.75 % (2882859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.75 % (2882859)CaDiCaL version: 2.1.3
% 12.57/2.75 % (2882859)Termination reason: Instruction limit
% 12.57/2.75 % (2882859)Termination phase: Saturation
% 12.57/2.75 % (2882859)Time elapsed: 0.077 s
% 12.57/2.75 % (2882859)Peak memory usage: 93 MB
% 12.57/2.75 % (2882859)Instructions burned: 131 (million)
% 12.57/2.75 % (2882866)lrs+10_1_sil=8000:sp=occurrence:random_seed=1701160521:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.57/2.75 % (2882866)Instruction limit reached!
% 12.57/2.75 % (2882866)------------------------------
% 12.57/2.75 % (2882866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.75 % (2882866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.75 % (2882866)CaDiCaL version: 2.1.3
% 12.57/2.75 % (2882866)Termination reason: Instruction limit
% 12.57/2.75 % (2882866)Termination phase: Saturation
% 12.57/2.75 % (2882866)Time elapsed: 0.101 s
% 12.57/2.75 % (2882866)Peak memory usage: 92 MB
% 12.57/2.75 % (2882866)Instructions burned: 288 (million)
% 15.53/3.42 % (2882868)lrs+10_1_sil=32000:urr=on:br=off:random_seed=404825393:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 15.53/3.42 % (2882869)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1955376340:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.53/3.42 % (2882856)------------------------------
% 15.53/3.42 % (2882856)------------------------------
% 15.53/3.42 % (2882871)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=3732664993:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 15.53/3.42 % (2882868)Instruction limit reached!
% 15.53/3.42 % (2882868)------------------------------
% 15.53/3.42 % (2882868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882868)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882868)Termination reason: Instruction limit
% 15.53/3.42 % (2882868)Termination phase: Saturation
% 15.53/3.42 % (2882868)Time elapsed: 0.080 s
% 15.53/3.42 % (2882868)Peak memory usage: 89 MB
% 15.53/3.42 % (2882868)Instructions burned: 157 (million)
% 15.53/3.42 % (2882871)Instruction limit reached!
% 15.53/3.42 % (2882871)------------------------------
% 15.53/3.42 % (2882871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882871)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882871)Termination reason: Instruction limit
% 15.53/3.42 % (2882871)Termination phase: Saturation
% 15.53/3.42 % (2882871)Time elapsed: 0.085 s
% 15.53/3.42 % (2882871)Peak memory usage: 93 MB
% 15.53/3.42 % (2882871)Instructions burned: 248 (million)
% 15.53/3.42 % (2882874)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1194287176:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 15.53/3.42 % (2882874)Refutation not found, incomplete strategy
% 15.53/3.42 % (2882874)------------------------------
% 15.53/3.42 % (2882874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882874)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882874)Termination reason: Refutation not found, incomplete strategy
% 15.53/3.42 % (2882874)Time elapsed: 0.004 s
% 15.53/3.42 % (2882874)Peak memory usage: 88 MB
% 15.53/3.42 % (2882874)Instructions burned: 5 (million)
% 15.53/3.42 % (2882869)Instruction limit reached!
% 15.53/3.42 % (2882869)------------------------------
% 15.53/3.42 % (2882869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882869)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882869)Termination reason: Instruction limit
% 15.53/3.42 % (2882869)Termination phase: Saturation
% 15.53/3.42 % (2882869)Time elapsed: 0.198 s
% 15.53/3.42 % (2882869)Peak memory usage: 92 MB
% 15.53/3.42 % (2882869)Instructions burned: 325 (million)
% 15.53/3.42 % (2882876)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=647756801:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 15.53/3.42 % (2882877)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3485685937:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 15.53/3.42 % (2882877)Instruction limit reached!
% 15.53/3.42 % (2882877)------------------------------
% 15.53/3.42 % (2882877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882877)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882877)Termination reason: Instruction limit
% 15.53/3.42 % (2882877)Termination phase: Saturation
% 15.53/3.42 % (2882877)Time elapsed: 0.041 s
% 15.53/3.42 % (2882877)Peak memory usage: 91 MB
% 15.53/3.42 % (2882877)Instructions burned: 114 (million)
% 15.53/3.42 % (2882879)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2486383549:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 15.53/3.42 % (2882879)Instruction limit reached!
% 15.53/3.42 % (2882879)------------------------------
% 15.53/3.42 % (2882879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882879)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882879)Termination reason: Instruction limit
% 15.53/3.42 % (2882879)Termination phase: Saturation
% 15.53/3.42 % (2882879)Time elapsed: 0.063 s
% 15.53/3.42 % (2882879)Peak memory usage: 89 MB
% 15.53/3.42 % (2882879)Instructions burned: 127 (million)
% 15.53/3.42 % (2882874)------------------------------
% 15.53/3.42 % (2882874)------------------------------
% 15.53/3.42 % (2882882)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3068317186:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 15.53/3.42 % (2882882)Instruction limit reached!
% 15.53/3.42 % (2882882)------------------------------
% 15.53/3.42 % (2882882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882882)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882882)Termination reason: Instruction limit
% 15.53/3.42 % (2882882)Termination phase: Saturation
% 15.53/3.42 % (2882882)Time elapsed: 0.042 s
% 15.53/3.42 % (2882882)Peak memory usage: 89 MB
% 15.53/3.42 % (2882882)Instructions burned: 115 (million)
% 15.53/3.42 % (2882884)lrs+10_1_sil=8000:sp=occurrence:random_seed=2618137840:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 15.53/3.42 % (2882885)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3472573663:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 15.53/3.42 % (2882885)Refutation not found, incomplete strategy
% 15.53/3.42 % (2882885)------------------------------
% 15.53/3.42 % (2882885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882885)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882885)Termination reason: Refutation not found, incomplete strategy
% 15.53/3.42 % (2882885)Time elapsed: 0.007 s
% 15.53/3.42 % (2882885)Peak memory usage: 88 MB
% 15.53/3.42 % (2882885)Instructions burned: 11 (million)
% 15.53/3.42 % (2882887)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=354124506:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 15.53/3.42 % (2882885)------------------------------
% 15.53/3.42 % (2882885)------------------------------
% 15.53/3.42 % (2882891)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3126949273:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 15.53/3.42 % (2882891)Instruction limit reached!
% 15.53/3.42 % (2882891)------------------------------
% 15.53/3.42 % (2882891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882891)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882891)Termination reason: Instruction limit
% 15.53/3.42 % (2882891)Termination phase: Saturation
% 15.53/3.42 % (2882891)Time elapsed: 0.079 s
% 15.53/3.42 % (2882891)Peak memory usage: 92 MB
% 15.53/3.42 % (2882891)Instructions burned: 135 (million)
% 15.53/3.42 % (2882884)Instruction limit reached!
% 15.53/3.42 % (2882884)------------------------------
% 15.53/3.42 % (2882884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882884)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882884)Termination reason: Instruction limit
% 15.53/3.42 % (2882884)Termination phase: Saturation
% 15.53/3.42 % (2882884)Time elapsed: 0.560 s
% 15.53/3.42 % (2882884)Peak memory usage: 101 MB
% 15.53/3.42 % (2882884)Instructions burned: 908 (million)
% 15.53/3.42 % (2882893)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2697262486:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 15.53/3.42 % (2882894)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2931617085:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 15.53/3.42 % (2882893)Instruction limit reached!
% 15.53/3.42 % (2882893)------------------------------
% 15.53/3.42 % (2882893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882893)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882893)Termination reason: Instruction limit
% 15.53/3.42 % (2882893)Termination phase: Saturation
% 15.53/3.42 % (2882893)Time elapsed: 0.373 s
% 15.53/3.42 % (2882893)Peak memory usage: 99 MB
% 15.53/3.42 % (2882893)Instructions burned: 593 (million)
% 15.53/3.42 % (2882897)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=1894756267:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 15.53/3.42 % (2882897)Instruction limit reached!
% 15.53/3.42 % (2882897)------------------------------
% 15.53/3.42 % (2882897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882897)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882897)Termination reason: Instruction limit
% 15.53/3.42 % (2882897)Termination phase: Saturation
% 15.53/3.42 % (2882897)Time elapsed: 0.078 s
% 15.53/3.42 % (2882897)Peak memory usage: 91 MB
% 15.53/3.42 % (2882897)Instructions burned: 126 (million)
% 15.53/3.42 % (2882876)Instruction limit reached!
% 15.53/3.42 % (2882876)------------------------------
% 15.53/3.42 % (2882876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882876)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882876)Termination reason: Instruction limit
% 15.53/3.42 % (2882876)Termination phase: Saturation
% 15.53/3.42 % (2882876)Time elapsed: 1.526 s
% 15.53/3.42 % (2882876)Peak memory usage: 142 MB
% 15.53/3.42 % (2882876)Instructions burned: 2351 (million)
% 15.53/3.42 % (2882899)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1949618366:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 15.53/3.42 % (2882900)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2227476235:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 15.53/3.42 % (2882900)Refutation not found, incomplete strategy
% 15.53/3.42 % (2882900)------------------------------
% 15.53/3.42 % (2882900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882900)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882900)Termination reason: Refutation not found, incomplete strategy
% 15.53/3.42 % (2882900)Time elapsed: 0.002 s
% 15.53/3.42 % (2882900)Peak memory usage: 88 MB
% 15.53/3.42 % (2882900)Instructions burned: 1 (million)
% 15.53/3.42 % (2882855)First to succeed.
% 15.53/3.42 % (2882855)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2882848"
% 15.53/3.42 % (2882899)Instruction limit reached!
% 15.53/3.42 % (2882899)------------------------------
% 15.53/3.42 % (2882899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882899)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882899)Termination reason: Instruction limit
% 15.53/3.42 % (2882899)Termination phase: Saturation
% 15.53/3.42 % (2882899)Time elapsed: 0.090 s
% 15.53/3.42 % (2882899)Peak memory usage: 91 MB
% 15.53/3.42 % (2882899)Instructions burned: 134 (million)
% 15.53/3.42 % (2882903)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=165925289:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 15.53/3.42 % (2882903)Refutation not found, incomplete strategy
% 15.53/3.42 % (2882903)------------------------------
% 15.53/3.42 % (2882903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.42 % (2882903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.42 % (2882903)CaDiCaL version: 2.1.3
% 15.53/3.42 % (2882903)Termination reason: Refutation not found, incomplete strategy
% 15.53/3.42 % (2882903)Time elapsed: 0.005 s
% 15.53/3.42 % (2882903)Peak memory usage: 89 MB
% 15.53/3.42 % (2882903)Instructions burned: 6 (million)
% 15.53/3.42 % (2882900)------------------------------
% 15.53/3.42 % (2882900)------------------------------
% 15.53/3.42 % (2882855)Refutation found. Thanks to Tanya!
% 15.53/3.42 % SZS status Theorem for theBenchmark
% 15.53/3.42 % SZS output start Proof for theBenchmark
% See solution above
% 18.69/3.62 % (2882855)------------------------------
% 18.69/3.62 % (2882855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.69/3.62 % (2882855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.69/3.62 % (2882855)CaDiCaL version: 2.1.3
% 18.69/3.62 % (2882855)Termination reason: Refutation
% 18.69/3.62 % (2882855)Time elapsed: 2.148 s
% 18.69/3.62 % (2882855)Peak memory usage: 148 MB
% 18.69/3.62 % (2882855)Instructions burned: 3034 (million)
% 18.69/3.62 % (2882855)------------------------------
% 18.69/3.62 % (2882855)------------------------------
% 18.69/3.62 % (2882848)Success in time 2.558 s
% 18.69/3.62 % Vampire exiting
%------------------------------------------------------------------------------