%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG214+4 : 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 : n019.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 09:19:20 AM UTC 2026
% Result : Theorem 11.58s 3.45s
% Output : Refutation 12.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 23
% Syntax : Number of formulae : 210 ( 59 unt; 19 def)
% Number of atoms : 2052 ( 49 equ)
% Maximal formula atoms : 26 ( 9 avg)
% Number of connectives : 3341 (1499 ~;1665 |; 134 &)
% ( 22 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 11 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 20 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 254 ( 0 sgn 244 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5328,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f24416,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ! [X4] :
( m2_rmod_4(X4,X0,X1,X2)
=> ( r1_tarski(X2,X3)
=> m2_rmod_4(X4,X0,X1,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_rmod_4) ).
fof(f24499,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( v1_rmod_5(X2,X0,X1)
<=> ! [X3] :
( m2_rmod_4(X3,X0,X1,X2)
=> ( k5_rmod_4(X0,X1,X3) = k1_rlvect_1(X1)
=> k2_rmod_4(X0,X1,X3) = k1_xboole_0 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_rmod_5) ).
fof(f24501,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ( ( r1_tarski(X2,X3)
& v1_rmod_5(X3,X0,X1) )
=> v1_rmod_5(X2,X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_rmod_5) ).
fof(f24502,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ( ( r1_tarski(X2,X3)
& v1_rmod_5(X3,X0,X1) )
=> v1_rmod_5(X2,X0,X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f24501]) ).
fof(f24512,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_rmod_5(X2,X0,X1)
<=> ! [X3] :
( k2_rmod_4(X0,X1,X3) = k1_xboole_0
| k1_rlvect_1(X1) != k5_rmod_4(X0,X1,X3)
| ~ m2_rmod_4(X3,X0,X1,X2) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f24499]) ).
fof(f24513,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_rmod_5(X2,X0,X1)
<=> ! [X3] :
( k2_rmod_4(X0,X1,X3) = k1_xboole_0
| k1_rlvect_1(X1) != k5_rmod_4(X0,X1,X3)
| ~ m2_rmod_4(X3,X0,X1,X2) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(flattening,[],[f24512]) ).
fof(f24514,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ~ v1_rmod_5(X2,X0,X1)
& r1_tarski(X2,X3)
& v1_rmod_5(X3,X0,X1)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f24502]) ).
fof(f24515,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ~ v1_rmod_5(X2,X0,X1)
& r1_tarski(X2,X3)
& v1_rmod_5(X3,X0,X1)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) ),
inference(flattening,[],[f24514]) ).
fof(f24611,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( m2_rmod_4(X4,X0,X1,X3)
| ~ r1_tarski(X2,X3)
| ~ m2_rmod_4(X4,X0,X1,X2) )
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f24416]) ).
fof(f24612,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( m2_rmod_4(X4,X0,X1,X3)
| ~ r1_tarski(X2,X3)
| ~ m2_rmod_4(X4,X0,X1,X2) )
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(flattening,[],[f24611]) ).
fof(f24660,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_rmod_5(X2,X0,X1)
| ? [X3] :
( k1_xboole_0 != k2_rmod_4(X0,X1,X3)
& k1_rlvect_1(X1) = k5_rmod_4(X0,X1,X3)
& m2_rmod_4(X3,X0,X1,X2) ) )
& ( ! [X3] :
( k2_rmod_4(X0,X1,X3) = k1_xboole_0
| k1_rlvect_1(X1) != k5_rmod_4(X0,X1,X3)
| ~ m2_rmod_4(X3,X0,X1,X2) )
| ~ v1_rmod_5(X2,X0,X1) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(nnf_transformation,[],[f24513]) ).
fof(f24661,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_rmod_5(X2,X0,X1)
| ? [X3] :
( k1_xboole_0 != k2_rmod_4(X0,X1,X3)
& k1_rlvect_1(X1) = k5_rmod_4(X0,X1,X3)
& m2_rmod_4(X3,X0,X1,X2) ) )
& ( ! [X4] :
( k1_xboole_0 = k2_rmod_4(X0,X1,X4)
| k1_rlvect_1(X1) != k5_rmod_4(X0,X1,X4)
| ~ m2_rmod_4(X4,X0,X1,X2) )
| ~ v1_rmod_5(X2,X0,X1) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(rectify,[],[f24660]) ).
fof(f24662,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_rmod_5(X2,X0,X1)
| ( k1_xboole_0 != k2_rmod_4(X0,X1,sK0(X0,X1,X2))
& k1_rlvect_1(X1) = k5_rmod_4(X0,X1,sK0(X0,X1,X2))
& m2_rmod_4(sK0(X0,X1,X2),X0,X1,X2) ) )
& ( ! [X4] :
( k1_xboole_0 = k2_rmod_4(X0,X1,X4)
| k1_rlvect_1(X1) != k5_rmod_4(X0,X1,X4)
| ~ m2_rmod_4(X4,X0,X1,X2) )
| ~ v1_rmod_5(X2,X0,X1) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1,X2))],[f24661]) ).
fof(f24663,plain,
( ~ v1_rmod_5(sK3,sK1,sK2)
& r1_tarski(sK3,sK4)
& v1_rmod_5(sK4,sK1,sK2)
& m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
& m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2)))
& ~ v3_struct_0(sK2)
& v3_rlvect_1(sK2)
& v4_rlvect_1(sK2)
& v5_rlvect_1(sK2)
& v6_rlvect_1(sK2)
& v5_vectsp_2(sK2,sK1)
& l1_vectsp_2(sK2,sK1)
& ~ v3_struct_0(sK1)
& v3_rlvect_1(sK1)
& v4_rlvect_1(sK1)
& v5_rlvect_1(sK1)
& v6_rlvect_1(sK1)
& v4_group_1(sK1)
& v6_vectsp_1(sK1)
& v7_vectsp_1(sK1)
& v8_vectsp_1(sK1)
& l3_vectsp_1(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4)],[f24515]) ).
fof(f24714,plain,
! [X2,X0,X1,X4] :
( k1_xboole_0 = k2_rmod_4(X0,X1,X4)
| k1_rlvect_1(X1) != k5_rmod_4(X0,X1,X4)
| ~ m2_rmod_4(X4,X0,X1,X2)
| ~ v1_rmod_5(X2,X0,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f24662]) ).
fof(f24715,plain,
! [X2,X0,X1] :
( v1_rmod_5(X2,X0,X1)
| m2_rmod_4(sK0(X0,X1,X2),X0,X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f24662]) ).
fof(f24716,plain,
! [X2,X0,X1] :
( v1_rmod_5(X2,X0,X1)
| k1_rlvect_1(X1) = k5_rmod_4(X0,X1,sK0(X0,X1,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f24662]) ).
fof(f24717,plain,
! [X2,X0,X1] :
( v1_rmod_5(X2,X0,X1)
| k1_xboole_0 != k2_rmod_4(X0,X1,sK0(X0,X1,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f24662]) ).
fof(f24718,plain,
l3_vectsp_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24719,plain,
v8_vectsp_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24720,plain,
v7_vectsp_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24721,plain,
v6_vectsp_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24722,plain,
v4_group_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24723,plain,
v6_rlvect_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24724,plain,
v5_rlvect_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24725,plain,
v4_rlvect_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24726,plain,
v3_rlvect_1(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24727,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24728,plain,
l1_vectsp_2(sK2,sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24729,plain,
v5_vectsp_2(sK2,sK1),
inference(cnf_transformation,[],[f24663]) ).
fof(f24730,plain,
v6_rlvect_1(sK2),
inference(cnf_transformation,[],[f24663]) ).
fof(f24731,plain,
v5_rlvect_1(sK2),
inference(cnf_transformation,[],[f24663]) ).
fof(f24732,plain,
v4_rlvect_1(sK2),
inference(cnf_transformation,[],[f24663]) ).
fof(f24733,plain,
v3_rlvect_1(sK2),
inference(cnf_transformation,[],[f24663]) ).
fof(f24734,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f24663]) ).
fof(f24735,plain,
m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf_transformation,[],[f24663]) ).
fof(f24736,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf_transformation,[],[f24663]) ).
fof(f24737,plain,
v1_rmod_5(sK4,sK1,sK2),
inference(cnf_transformation,[],[f24663]) ).
fof(f24738,plain,
r1_tarski(sK3,sK4),
inference(cnf_transformation,[],[f24663]) ).
fof(f24739,plain,
~ v1_rmod_5(sK3,sK1,sK2),
inference(cnf_transformation,[],[f24663]) ).
fof(f24831,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f5328]) ).
fof(f24863,plain,
! [X2,X3,X0,X1,X4] :
( m2_rmod_4(X4,X0,X1,X3)
| ~ r1_tarski(X2,X3)
| ~ m2_rmod_4(X4,X0,X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f24612]) ).
fof(f24915,plain,
! [X2,X0,X1] :
( v1_rmod_5(X2,X0,X1)
| np__0 != k2_rmod_4(X0,X1,sK0(X0,X1,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(definition_unfolding,[],[f24717,f24831]) ).
fof(f24916,plain,
! [X2,X0,X1,X4] :
( np__0 = k2_rmod_4(X0,X1,X4)
| k1_rlvect_1(X1) != k5_rmod_4(X0,X1,X4)
| ~ m2_rmod_4(X4,X0,X1,X2)
| ~ v1_rmod_5(X2,X0,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(definition_unfolding,[],[f24714,f24831]) ).
fof(f25005,definition,
( spl52_1
<=> v3_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl52_1])],[avatar_definition]) ).
fof(f25007,plain,
( ~ v3_struct_0(sK2)
| spl52_1 ),
inference(avatar_component_clause,[],[f25005]) ).
fof(f25008,plain,
~ spl52_1,
inference(avatar_split_clause,[],[f24734,f25005]) ).
fof(f25010,definition,
( spl52_2
<=> v3_struct_0(sK1) ),
introduced(definition,[new_symbols(definition,[spl52_2])],[avatar_definition]) ).
fof(f25012,plain,
( ~ v3_struct_0(sK1)
| spl52_2 ),
inference(avatar_component_clause,[],[f25010]) ).
fof(f25013,plain,
~ spl52_2,
inference(avatar_split_clause,[],[f24727,f25010]) ).
fof(f27063,definition,
( spl52_3
<=> l1_vectsp_2(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl52_3])],[avatar_definition]) ).
fof(f27065,plain,
( l1_vectsp_2(sK2,sK1)
| ~ spl52_3 ),
inference(avatar_component_clause,[],[f27063]) ).
fof(f27066,plain,
spl52_3,
inference(avatar_split_clause,[],[f24728,f27063]) ).
fof(f27128,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| ~ spl52_3 ),
inference(resolution,[],[f27065,f24915]) ).
fof(f27149,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27128,f25007]) ).
fof(f27221,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27149,f24733]) ).
fof(f27293,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27221,f24732]) ).
fof(f27365,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27293,f24731]) ).
fof(f27437,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27365,f24730]) ).
fof(f27509,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27437,f24729]) ).
fof(f27581,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27509,f25012]) ).
fof(f27650,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27581,f24726]) ).
fof(f27719,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27650,f24725]) ).
fof(f27788,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27719,f24724]) ).
fof(f27857,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27788,f24723]) ).
fof(f27922,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27857,f24722]) ).
fof(f27987,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27922,f24721]) ).
fof(f28052,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f27987,f24720]) ).
fof(f28117,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f28052,f24719]) ).
fof(f28182,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f28117,f24718]) ).
fof(f28263,definition,
( spl52_4
<=> ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl52_4])],[avatar_definition]) ).
fof(f28264,plain,
( ! [X0] :
( np__0 != k2_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl52_4 ),
inference(avatar_component_clause,[],[f28263]) ).
fof(f28265,plain,
( spl52_4
| spl52_1
| spl52_2
| ~ spl52_3 ),
inference(avatar_split_clause,[],[f28182,f27063,f25010,f25005,f28263]) ).
fof(f28266,plain,
( ! [X0,X1] :
( np__0 != np__0
| v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| k1_rlvect_1(sK2) != k5_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| ~ spl52_4 ),
inference(superposition,[],[f28264,f24916]) ).
fof(f28267,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| k1_rlvect_1(sK2) != k5_rmod_4(sK1,sK2,sK0(sK1,sK2,X0))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| ~ spl52_4 ),
inference(trivial_inequality_removal,[],[f28266]) ).
fof(f28268,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28267,f24716]) ).
fof(f28269,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28268,f25007]) ).
fof(f28270,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28269,f24733]) ).
fof(f28271,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28270,f24732]) ).
fof(f28272,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28271,f24731]) ).
fof(f28273,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28272,f24730]) ).
fof(f28274,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28273,f24729]) ).
fof(f28275,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28274,f27065]) ).
fof(f28276,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28275,f25012]) ).
fof(f28277,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28276,f24726]) ).
fof(f28278,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28277,f24725]) ).
fof(f28279,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28278,f24724]) ).
fof(f28280,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28279,f24723]) ).
fof(f28281,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28280,f24722]) ).
fof(f28282,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28281,f24721]) ).
fof(f28283,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28282,f24720]) ).
fof(f28284,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28283,f24719]) ).
fof(f28285,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2))) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f28284,f24718]) ).
fof(f28287,definition,
( spl52_5
<=> m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl52_5])],[avatar_definition]) ).
fof(f28289,plain,
( m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ spl52_5 ),
inference(avatar_component_clause,[],[f28287]) ).
fof(f28290,plain,
spl52_5,
inference(avatar_split_clause,[],[f24735,f28287]) ).
fof(f28292,definition,
( spl52_6
<=> ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl52_6])],[avatar_definition]) ).
fof(f28293,plain,
( ! [X0,X1] :
( ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl52_6 ),
inference(avatar_component_clause,[],[f28292]) ).
fof(f28294,plain,
( spl52_6
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(avatar_split_clause,[],[f28285,f28263,f27063,f25010,f25005,f28292]) ).
fof(f28298,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| ~ spl52_6 ),
inference(resolution,[],[f28293,f24863]) ).
fof(f28299,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| ~ spl52_6 ),
inference(duplicate_literal_removal,[],[f28298]) ).
fof(f28302,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28299,f25007]) ).
fof(f28305,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28302,f24733]) ).
fof(f28308,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28305,f24732]) ).
fof(f28311,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28308,f24731]) ).
fof(f28314,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28311,f24730]) ).
fof(f28317,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28314,f24729]) ).
fof(f28320,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28317,f27065]) ).
fof(f28323,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28320,f25012]) ).
fof(f28326,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28323,f24726]) ).
fof(f28329,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28326,f24725]) ).
fof(f28332,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28329,f24724]) ).
fof(f28335,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28332,f24723]) ).
fof(f28338,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28335,f24722]) ).
fof(f28341,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28338,f24721]) ).
fof(f28344,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28341,f24720]) ).
fof(f28347,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28344,f24719]) ).
fof(f28350,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2))) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f28347,f24718]) ).
fof(f28446,definition,
( spl52_7
<=> v5_vectsp_2(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl52_7])],[avatar_definition]) ).
fof(f28448,plain,
( v5_vectsp_2(sK2,sK1)
| ~ spl52_7 ),
inference(avatar_component_clause,[],[f28446]) ).
fof(f28449,plain,
spl52_7,
inference(avatar_split_clause,[],[f24729,f28446]) ).
fof(f28560,definition,
( spl52_8
<=> v1_rmod_5(sK4,sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl52_8])],[avatar_definition]) ).
fof(f28562,plain,
( v1_rmod_5(sK4,sK1,sK2)
| ~ spl52_8 ),
inference(avatar_component_clause,[],[f28560]) ).
fof(f28563,plain,
spl52_8,
inference(avatar_split_clause,[],[f24737,f28560]) ).
fof(f28584,definition,
( spl52_9
<=> v1_rmod_5(sK3,sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl52_9])],[avatar_definition]) ).
fof(f28586,plain,
( ~ v1_rmod_5(sK3,sK1,sK2)
| spl52_9 ),
inference(avatar_component_clause,[],[f28584]) ).
fof(f28587,plain,
~ spl52_9,
inference(avatar_split_clause,[],[f24739,f28584]) ).
fof(f28589,definition,
( spl52_10
<=> v4_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl52_10])],[avatar_definition]) ).
fof(f28591,plain,
( v4_rlvect_1(sK2)
| ~ spl52_10 ),
inference(avatar_component_clause,[],[f28589]) ).
fof(f28592,plain,
spl52_10,
inference(avatar_split_clause,[],[f24732,f28589]) ).
fof(f28594,definition,
( spl52_11
<=> l3_vectsp_1(sK1) ),
introduced(definition,[new_symbols(definition,[spl52_11])],[avatar_definition]) ).
fof(f28596,plain,
( l3_vectsp_1(sK1)
| ~ spl52_11 ),
inference(avatar_component_clause,[],[f28594]) ).
fof(f28597,plain,
spl52_11,
inference(avatar_split_clause,[],[f24718,f28594]) ).
fof(f28599,definition,
( spl52_12
<=> v4_group_1(sK1) ),
introduced(definition,[new_symbols(definition,[spl52_12])],[avatar_definition]) ).
fof(f28601,plain,
( v4_group_1(sK1)
| ~ spl52_12 ),
inference(avatar_component_clause,[],[f28599]) ).
fof(f28602,plain,
spl52_12,
inference(avatar_split_clause,[],[f24722,f28599]) ).
fof(f28604,definition,
( spl52_13
<=> v5_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl52_13])],[avatar_definition]) ).
fof(f28606,plain,
( v5_rlvect_1(sK2)
| ~ spl52_13 ),
inference(avatar_component_clause,[],[f28604]) ).
fof(f28607,plain,
spl52_13,
inference(avatar_split_clause,[],[f24731,f28604]) ).
fof(f28671,definition,
( spl52_15
<=> r1_tarski(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl52_15])],[avatar_definition]) ).
fof(f28673,plain,
( r1_tarski(sK3,sK4)
| ~ spl52_15 ),
inference(avatar_component_clause,[],[f28671]) ).
fof(f28674,plain,
spl52_15,
inference(avatar_split_clause,[],[f24738,f28671]) ).
fof(f28709,definition,
( spl52_16
<=> v6_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl52_16])],[avatar_definition]) ).
fof(f28711,plain,
( v6_rlvect_1(sK2)
| ~ spl52_16 ),
inference(avatar_component_clause,[],[f28709]) ).
fof(f28712,plain,
spl52_16,
inference(avatar_split_clause,[],[f24730,f28709]) ).
fof(f28888,definition,
( spl52_17
<=> ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl52_17])],[avatar_definition]) ).
fof(f28889,plain,
( ! [X2,X0,X1] :
( ~ m2_rmod_4(sK0(sK1,sK2,X0),sK1,sK2,X2)
| v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X2,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl52_17 ),
inference(avatar_component_clause,[],[f28888]) ).
fof(f28890,plain,
( spl52_17
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6 ),
inference(avatar_split_clause,[],[f28350,f28292,f27063,f25010,f25005,f28888]) ).
fof(f28891,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v1_rmod_5(X0,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| ~ spl52_17 ),
inference(resolution,[],[f28889,f24715]) ).
fof(f28897,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| ~ spl52_17 ),
inference(duplicate_literal_removal,[],[f28891]) ).
fof(f28900,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28897,f25007]) ).
fof(f28903,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28900,f24733]) ).
fof(f28906,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_10
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28903,f28591]) ).
fof(f28909,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_rlvect_1(sK2)
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_10
| ~ spl52_13
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28906,f28606]) ).
fof(f28912,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_10
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28909,f28711]) ).
fof(f28915,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_vectsp_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_7
| ~ spl52_10
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28912,f28448]) ).
fof(f28918,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28915,f27065]) ).
fof(f28921,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28918,f25012]) ).
fof(f28924,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28921,f24726]) ).
fof(f28927,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28924,f24725]) ).
fof(f28930,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_rlvect_1(sK1)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28927,f24724]) ).
fof(f28933,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28930,f24723]) ).
fof(f28936,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_12
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28933,f28601]) ).
fof(f28939,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_12
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28936,f24721]) ).
fof(f28942,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v8_vectsp_1(sK1)
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_12
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28939,f24720]) ).
fof(f28945,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_vectsp_1(sK1) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_12
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28942,f24719]) ).
fof(f28948,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_11
| ~ spl52_12
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(forward_subsumption_resolution,[],[f28945,f28596]) ).
fof(f28950,definition,
( spl52_18
<=> ! [X0,X1] :
( v1_rmod_5(X0,sK1,sK2)
| ~ v1_rmod_5(X1,sK1,sK2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl52_18])],[avatar_definition]) ).
fof(f28951,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_rmod_5(X1,sK1,sK2)
| v1_rmod_5(X0,sK1,sK2)
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl52_18 ),
inference(avatar_component_clause,[],[f28950]) ).
fof(f28952,plain,
( spl52_18
| spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_11
| ~ spl52_12
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17 ),
inference(avatar_split_clause,[],[f28948,f28888,f28709,f28604,f28599,f28594,f28589,f28446,f27063,f25010,f25005,f28950]) ).
fof(f30300,definition,
( spl52_24
<=> m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl52_24])],[avatar_definition]) ).
fof(f30302,plain,
( m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ spl52_24 ),
inference(avatar_component_clause,[],[f30300]) ).
fof(f30303,plain,
spl52_24,
inference(avatar_split_clause,[],[f24736,f30300]) ).
fof(f30304,plain,
( ! [X0] :
( ~ v1_rmod_5(sK4,sK1,sK2)
| v1_rmod_5(X0,sK1,sK2)
| ~ r1_tarski(X0,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl52_18
| ~ spl52_24 ),
inference(resolution,[],[f30302,f28951]) ).
fof(f30356,plain,
( ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| ~ r1_tarski(X0,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl52_8
| ~ spl52_18
| ~ spl52_24 ),
inference(forward_subsumption_resolution,[],[f30304,f28562]) ).
fof(f30398,definition,
( spl52_25
<=> ! [X0] :
( v1_rmod_5(X0,sK1,sK2)
| ~ r1_tarski(X0,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl52_25])],[avatar_definition]) ).
fof(f30399,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r1_tarski(X0,sK4)
| v1_rmod_5(X0,sK1,sK2) )
| ~ spl52_25 ),
inference(avatar_component_clause,[],[f30398]) ).
fof(f30400,plain,
( spl52_25
| ~ spl52_8
| ~ spl52_18
| ~ spl52_24 ),
inference(avatar_split_clause,[],[f30356,f30300,f28950,f28560,f30398]) ).
fof(f30407,plain,
( ~ r1_tarski(sK3,sK4)
| v1_rmod_5(sK3,sK1,sK2)
| ~ spl52_5
| ~ spl52_25 ),
inference(resolution,[],[f30399,f28289]) ).
fof(f30420,plain,
( v1_rmod_5(sK3,sK1,sK2)
| ~ spl52_5
| ~ spl52_15
| ~ spl52_25 ),
inference(forward_subsumption_resolution,[],[f30407,f28673]) ).
fof(f30425,plain,
( $false
| ~ spl52_5
| spl52_9
| ~ spl52_15
| ~ spl52_25 ),
inference(forward_subsumption_resolution,[],[f30420,f28586]) ).
fof(f30426,plain,
( ~ spl52_5
| spl52_9
| ~ spl52_15
| ~ spl52_25 ),
inference(avatar_contradiction_clause,[],[f30425]) ).
cnf(s1,plain,
~ spl52_1,
inference(sat_conversion,[],[f25008]) ).
cnf(s2,plain,
~ spl52_2,
inference(sat_conversion,[],[f25013]) ).
cnf(s3,plain,
spl52_3,
inference(sat_conversion,[],[f27066]) ).
cnf(s4,plain,
( spl52_1
| spl52_2
| ~ spl52_3
| spl52_4 ),
inference(sat_conversion,[],[f28265]) ).
cnf(s5,plain,
spl52_5,
inference(sat_conversion,[],[f28290]) ).
cnf(s6,plain,
( spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_4
| spl52_6 ),
inference(sat_conversion,[],[f28294]) ).
cnf(s7,plain,
spl52_7,
inference(sat_conversion,[],[f28449]) ).
cnf(s8,plain,
spl52_8,
inference(sat_conversion,[],[f28563]) ).
cnf(s9,plain,
~ spl52_9,
inference(sat_conversion,[],[f28587]) ).
cnf(s10,plain,
spl52_10,
inference(sat_conversion,[],[f28592]) ).
cnf(s11,plain,
spl52_11,
inference(sat_conversion,[],[f28597]) ).
cnf(s12,plain,
spl52_12,
inference(sat_conversion,[],[f28602]) ).
cnf(s13,plain,
spl52_13,
inference(sat_conversion,[],[f28607]) ).
cnf(s15,plain,
spl52_15,
inference(sat_conversion,[],[f28674]) ).
cnf(s16,plain,
spl52_16,
inference(sat_conversion,[],[f28712]) ).
cnf(s17,plain,
( spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_6
| spl52_17 ),
inference(sat_conversion,[],[f28890]) ).
cnf(s18,plain,
( spl52_1
| spl52_2
| ~ spl52_3
| ~ spl52_7
| ~ spl52_10
| ~ spl52_11
| ~ spl52_12
| ~ spl52_13
| ~ spl52_16
| ~ spl52_17
| spl52_18 ),
inference(sat_conversion,[],[f28952]) ).
cnf(s24,plain,
spl52_24,
inference(sat_conversion,[],[f30303]) ).
cnf(s25,plain,
( ~ spl52_8
| ~ spl52_18
| ~ spl52_24
| spl52_25 ),
inference(sat_conversion,[],[f30400]) ).
cnf(s26,plain,
( ~ spl52_5
| spl52_9
| ~ spl52_15
| ~ spl52_25 ),
inference(sat_conversion,[],[f30426]) ).
cnf(s27,plain,
~ spl52_25,
inference(rat,[],[s26,s9,s15,s5]) ).
cnf(s28,plain,
~ spl52_18,
inference(rat,[],[s25,s8,s24,s27]) ).
cnf(s29,plain,
~ spl52_17,
inference(rat,[],[s18,s28,s2,s16,s13,s12,s11,s10,s7,s3,s1]) ).
cnf(s30,plain,
~ spl52_6,
inference(rat,[],[s17,s29,s2,s3,s1]) ).
cnf(s32,plain,
~ spl52_4,
inference(rat,[],[s6,s30,s2,s3,s1]) ).
cnf(s33,plain,
$false,
inference(rat,[],[s4,s2,s3,s32,s1]) ).
fof(f30432,plain,
$false,
inference(avatar_sat_refutation,[],[s33]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG214+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n019.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:44:38 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.58/3.45 % (156928)Detected formulas, will run a generic FOF schedule.
% 11.58/3.45 % (156934)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=3655855976:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2986 on theBenchmark for (2986ds/134677Mi)
% 11.58/3.45 % (156935)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=76726650:i=141695:sd=1:nm=32:gsp=on:ss=included_2986 on theBenchmark for (2986ds/141695Mi)
% 11.58/3.45 % (156936)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2653776275:i=109:sd=1:ins=1:gsp=on:ss=axioms_2986 on theBenchmark for (2986ds/109Mi)
% 11.58/3.45 % (156933)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=895802330:i=141193_2986 on theBenchmark for (2986ds/141193Mi)
% 11.58/3.45 % (156939)dis-21_1_sil=8000:lcm=predicate:random_seed=1102124152:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2986 on theBenchmark for (2986ds/129Mi)
% 11.58/3.45 % (156937)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3012826634:i=119:av=off:ss=axioms_2986 on theBenchmark for (2986ds/119Mi)
% 11.58/3.45 % (156938)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3390772874:s2a=on:i=139:gtg=position_2986 on theBenchmark for (2986ds/139Mi)
% 11.58/3.45 % (156938)Instruction limit reached!
% 11.58/3.45 % (156938)------------------------------
% 11.58/3.45 % (156938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156938)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156938)Termination reason: Instruction limit
% 11.58/3.45 % (156938)Termination phase: Property scanning
% 11.58/3.45 % (156938)Time elapsed: 0.061 s
% 11.58/3.45 % (156938)Peak memory usage: 118 MB
% 11.58/3.45 % (156938)Instructions burned: 141 (million)
% 11.58/3.45 % (156936)Instruction limit reached!
% 11.58/3.45 % (156936)------------------------------
% 11.58/3.45 % (156936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156936)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156936)Termination reason: Instruction limit
% 11.58/3.45 % (156936)Termination phase: SInE selection
% 11.58/3.45 % (156936)Time elapsed: 0.082 s
% 11.58/3.45 % (156936)Peak memory usage: 118 MB
% 11.58/3.45 % (156936)Instructions burned: 110 (million)
% 11.58/3.45 % (156939)Instruction limit reached!
% 11.58/3.45 % (156939)------------------------------
% 11.58/3.45 % (156939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156939)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156939)Termination reason: Instruction limit
% 11.58/3.45 % (156939)Termination phase: SInE selection
% 11.58/3.45 % (156939)Time elapsed: 0.084 s
% 11.58/3.45 % (156939)Peak memory usage: 118 MB
% 11.58/3.45 % (156939)Instructions burned: 129 (million)
% 11.58/3.45 % (156937)Instruction limit reached!
% 11.58/3.45 % (156937)------------------------------
% 11.58/3.45 % (156937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156937)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156937)Termination reason: Instruction limit
% 11.58/3.45 % (156937)Termination phase: SInE selection
% 11.58/3.45 % (156937)Time elapsed: 0.086 s
% 11.58/3.45 % (156937)Peak memory usage: 118 MB
% 11.58/3.45 % (156937)Instructions burned: 120 (million)
% 11.58/3.45 % (156947)lrs+10_1_sil=8000:sp=occurrence:random_seed=1304578218:i=285:sd=3:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/285Mi)
% 11.58/3.45 % (156948)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3907474365:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/157Mi)
% 11.58/3.45 % (156949)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1038967553:i=325:sd=1:ss=axioms:sgt=32_2984 on theBenchmark for (2984ds/325Mi)
% 11.58/3.45 % (156950)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=544290246:s2a=on:i=248:s2at=1.23:gtg=position_2984 on theBenchmark for (2984ds/248Mi)
% 11.58/3.45 % (156948)Instruction limit reached!
% 11.58/3.45 % (156948)------------------------------
% 11.58/3.45 % (156948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156948)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156948)Termination reason: Instruction limit
% 11.58/3.45 % (156948)Termination phase: Property scanning
% 11.58/3.45 % (156948)Time elapsed: 0.067 s
% 11.58/3.45 % (156948)Peak memory usage: 118 MB
% 11.58/3.45 % (156948)Instructions burned: 158 (million)
% 11.58/3.45 % (156950)Instruction limit reached!
% 11.58/3.45 % (156950)------------------------------
% 11.58/3.45 % (156950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156950)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156950)Termination reason: Instruction limit
% 11.58/3.45 % (156950)Termination phase: Property scanning
% 11.58/3.45 % (156950)Time elapsed: 0.105 s
% 11.58/3.45 % (156950)Peak memory usage: 118 MB
% 11.58/3.45 % (156950)Instructions burned: 250 (million)
% 11.58/3.45 % (156947)Instruction limit reached!
% 11.58/3.45 % (156947)------------------------------
% 11.58/3.45 % (156947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156947)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156947)Termination reason: Instruction limit
% 11.58/3.45 % (156947)Termination phase: Saturation
% 11.58/3.45 % (156947)Time elapsed: 0.207 s
% 11.58/3.45 % (156947)Peak memory usage: 125 MB
% 11.58/3.45 % (156947)Instructions burned: 286 (million)
% 11.58/3.45 % (156955)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1381403500:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2982 on theBenchmark for (2982ds/294Mi)
% 11.58/3.45 % (156956)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4176509217:i=2350_2981 on theBenchmark for (2981ds/2350Mi)
% 11.58/3.45 % (156949)Instruction limit reached!
% 11.58/3.45 % (156949)------------------------------
% 11.58/3.45 % (156949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156949)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156949)Termination reason: Instruction limit
% 11.58/3.45 % (156949)Termination phase: Saturation
% 11.58/3.45 % (156949)Time elapsed: 0.249 s
% 11.58/3.45 % (156949)Peak memory usage: 124 MB
% 11.58/3.45 % (156949)Instructions burned: 326 (million)
% 11.58/3.45 % (156957)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1450926525:cts=off:i=113:fsr=off:ss=included:sgt=4_2980 on theBenchmark for (2980ds/113Mi)
% 11.58/3.45 % (156960)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=602358469:i=127:av=off:fsr=off:sup=off_2980 on theBenchmark for (2980ds/127Mi)
% 11.58/3.45 % (156955)Instruction limit reached!
% 11.58/3.45 % (156955)------------------------------
% 11.58/3.45 % (156955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156955)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156955)Termination reason: Instruction limit
% 11.58/3.45 % (156955)Termination phase: Property scanning
% 11.58/3.45 % (156955)Time elapsed: 0.208 s
% 11.58/3.45 % (156955)Peak memory usage: 123 MB
% 11.58/3.45 % (156955)Instructions burned: 296 (million)
% 11.58/3.45 % (156957)Instruction limit reached!
% 11.58/3.45 % (156957)------------------------------
% 11.58/3.45 % (156957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156957)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156957)Termination reason: Instruction limit
% 11.58/3.45 % (156957)Termination phase: SInE selection
% 11.58/3.45 % (156957)Time elapsed: 0.089 s
% 11.58/3.45 % (156957)Peak memory usage: 118 MB
% 11.58/3.45 % (156957)Instructions burned: 113 (million)
% 11.58/3.45 % (156960)Instruction limit reached!
% 11.58/3.45 % (156960)------------------------------
% 11.58/3.45 % (156960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156960)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156960)Termination reason: Instruction limit
% 11.58/3.45 % (156960)Termination phase: Preprocessing 1
% 11.58/3.45 % (156960)Time elapsed: 0.093 s
% 11.58/3.45 % (156960)Peak memory usage: 119 MB
% 11.58/3.45 % (156960)Instructions burned: 127 (million)
% 11.58/3.45 % (156963)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1517265278:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2978 on theBenchmark for (2978ds/114Mi)
% 11.58/3.45 % (156964)lrs+10_1_sil=8000:sp=occurrence:random_seed=3990036465:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2978 on theBenchmark for (2978ds/907Mi)
% 11.58/3.45 % (156963)Instruction limit reached!
% 11.58/3.45 % (156963)------------------------------
% 11.58/3.45 % (156963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156963)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156963)Termination reason: Instruction limit
% 11.58/3.45 % (156963)Termination phase: Property scanning
% 11.58/3.45 % (156963)Time elapsed: 0.051 s
% 11.58/3.45 % (156963)Peak memory usage: 118 MB
% 11.58/3.45 % (156963)Instructions burned: 114 (million)
% 11.58/3.45 % (156965)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3028696838:i=437:sd=1:aac=none:ss=included_2977 on theBenchmark for (2977ds/437Mi)
% 11.58/3.45 % (156968)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2898759349:i=5202:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/5202Mi)
% 11.58/3.45 % (156935)First to succeed.
% 11.58/3.45 % (156935)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-156928"
% 11.58/3.45 % (156965)Instruction limit reached!
% 11.58/3.45 % (156965)------------------------------
% 11.58/3.45 % (156965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/3.45 % (156965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/3.45 % (156965)CaDiCaL version: 2.1.3
% 11.58/3.45 % (156965)Termination reason: Instruction limit
% 11.58/3.45 % (156965)Termination phase: Saturation
% 11.58/3.45 % (156965)Time elapsed: 0.298 s
% 11.58/3.45 % (156965)Peak memory usage: 125 MB
% 11.58/3.45 % (156965)Instructions burned: 438 (million)
% 11.58/3.45 % (156935)Refutation found. Thanks to Tanya!
% 11.58/3.45 % SZS status Theorem for theBenchmark
% 11.58/3.45 % SZS output start Proof for theBenchmark
% See solution above
% 12.13/3.67 % (156935)------------------------------
% 12.13/3.67 % (156935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.13/3.67 % (156935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.13/3.67 % (156935)CaDiCaL version: 2.1.3
% 12.13/3.67 % (156935)Termination reason: Refutation
% 12.13/3.67 % (156935)Time elapsed: 1.115 s
% 12.13/3.67 % (156935)Peak memory usage: 180 MB
% 12.13/3.67 % (156935)Instructions burned: 2345 (million)
% 12.13/3.67 % (156935)------------------------------
% 12.13/3.67 % (156935)------------------------------
% 12.13/3.67 % (156928)Success in time 2.795 s
% 12.13/3.67 % Vampire exiting
%------------------------------------------------------------------------------