%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG214+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.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 4.46s 2.05s
% Output : Refutation 11.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 30
% Syntax : Number of formulae : 248 ( 73 unt; 27 def)
% Number of atoms : 2304 ( 54 equ)
% Maximal formula atoms : 26 ( 9 avg)
% Number of connectives : 3727 (1671 ~;1871 |; 134 &)
% ( 30 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 11 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 28 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 267 ( 0 sgn 257 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3360,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/sandbox/benchmark/theBenchmark.p',t25_rmod_4) ).
fof(f3443,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/sandbox/benchmark/theBenchmark.p',d1_rmod_5) ).
fof(f3445,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/sandbox/benchmark/theBenchmark.p',t2_rmod_5) ).
fof(f3446,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)],[f3445]) ).
fof(f3458,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,[],[f3443]) ).
fof(f3459,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,[],[f3458]) ).
fof(f3460,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,[],[f3446]) ).
fof(f3461,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,[],[f3460]) ).
fof(f3532,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,[],[f3360]) ).
fof(f3533,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,[],[f3532]) ).
fof(f3558,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,[],[f3459]) ).
fof(f3559,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,[],[f3558]) ).
fof(f3560,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_rmod_5(X2,X0,X1)
| ( k1_xboole_0 != k2_rmod_4(X0,X1,sK1(X0,X1,X2))
& k1_rlvect_1(X1) = k5_rmod_4(X0,X1,sK1(X0,X1,X2))
& m2_rmod_4(sK1(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,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f3559]) ).
fof(f3561,plain,
( ~ v1_rmod_5(sK4,sK2,sK3)
& r1_tarski(sK4,sK5)
& v1_rmod_5(sK5,sK2,sK3)
& m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK3)))
& m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
& ~ v3_struct_0(sK3)
& v3_rlvect_1(sK3)
& v4_rlvect_1(sK3)
& v5_rlvect_1(sK3)
& v6_rlvect_1(sK3)
& v5_vectsp_2(sK3,sK2)
& l1_vectsp_2(sK3,sK2)
& ~ v3_struct_0(sK2)
& v3_rlvect_1(sK2)
& v4_rlvect_1(sK2)
& v5_rlvect_1(sK2)
& v6_rlvect_1(sK2)
& v4_group_1(sK2)
& v6_vectsp_1(sK2)
& v7_vectsp_1(sK2)
& v8_vectsp_1(sK2)
& l3_vectsp_1(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f3461]) ).
fof(f3608,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,[],[f3560]) ).
fof(f3609,plain,
! [X2,X0,X1] :
( v1_rmod_5(X2,X0,X1)
| m2_rmod_4(sK1(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,[],[f3560]) ).
fof(f3610,plain,
! [X2,X0,X1] :
( v1_rmod_5(X2,X0,X1)
| k1_rlvect_1(X1) = k5_rmod_4(X0,X1,sK1(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,[],[f3560]) ).
fof(f3611,plain,
! [X2,X0,X1] :
( v1_rmod_5(X2,X0,X1)
| k1_xboole_0 != k2_rmod_4(X0,X1,sK1(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,[],[f3560]) ).
fof(f3612,plain,
l3_vectsp_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3613,plain,
v8_vectsp_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3614,plain,
v7_vectsp_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3615,plain,
v6_vectsp_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3616,plain,
v4_group_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3617,plain,
v6_rlvect_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3618,plain,
v5_rlvect_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3619,plain,
v4_rlvect_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3620,plain,
v3_rlvect_1(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3621,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3622,plain,
l1_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3623,plain,
v5_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f3561]) ).
fof(f3624,plain,
v6_rlvect_1(sK3),
inference(cnf_transformation,[],[f3561]) ).
fof(f3625,plain,
v5_rlvect_1(sK3),
inference(cnf_transformation,[],[f3561]) ).
fof(f3626,plain,
v4_rlvect_1(sK3),
inference(cnf_transformation,[],[f3561]) ).
fof(f3627,plain,
v3_rlvect_1(sK3),
inference(cnf_transformation,[],[f3561]) ).
fof(f3628,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f3561]) ).
fof(f3629,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3))),
inference(cnf_transformation,[],[f3561]) ).
fof(f3630,plain,
m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK3))),
inference(cnf_transformation,[],[f3561]) ).
fof(f3631,plain,
v1_rmod_5(sK5,sK2,sK3),
inference(cnf_transformation,[],[f3561]) ).
fof(f3632,plain,
r1_tarski(sK4,sK5),
inference(cnf_transformation,[],[f3561]) ).
fof(f3633,plain,
~ v1_rmod_5(sK4,sK2,sK3),
inference(cnf_transformation,[],[f3561]) ).
fof(f3770,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,[],[f3533]) ).
fof(f3805,definition,
( spl32_1
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
fof(f3807,plain,
( ~ v3_struct_0(sK3)
| spl32_1 ),
inference(avatar_component_clause,[],[f3805]) ).
fof(f3808,plain,
~ spl32_1,
inference(avatar_split_clause,[],[f3628,f3805]) ).
fof(f3810,definition,
( spl32_2
<=> v3_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
fof(f3812,plain,
( ~ v3_struct_0(sK2)
| spl32_2 ),
inference(avatar_component_clause,[],[f3810]) ).
fof(f3813,plain,
~ spl32_2,
inference(avatar_split_clause,[],[f3621,f3810]) ).
fof(f4593,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(resolution,[],[f3812,f3610]) ).
fof(f4873,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f4593,f3620]) ).
fof(f5019,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f4873,f3619]) ).
fof(f5165,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f5019,f3618]) ).
fof(f5311,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f5165,f3617]) ).
fof(f5404,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f5311,f3616]) ).
fof(f5491,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f5404,f3615]) ).
fof(f5575,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f5491,f3614]) ).
fof(f5659,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f5575,f3613]) ).
fof(f5742,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,X1)
| k1_rlvect_1(X1) = k5_rmod_4(sK2,X1,sK1(sK2,X1,X0))
| ~ m1_subset_1(X0,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,sK2)
| ~ l1_vectsp_2(X1,sK2) )
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f5659,f3612]) ).
fof(f5766,definition,
( spl32_3
<=> v1_rmod_5(sK5,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition]) ).
fof(f5768,plain,
( v1_rmod_5(sK5,sK2,sK3)
| ~ spl32_3 ),
inference(avatar_component_clause,[],[f5766]) ).
fof(f5769,plain,
spl32_3,
inference(avatar_split_clause,[],[f3631,f5766]) ).
fof(f5771,definition,
( spl32_4
<=> l1_vectsp_2(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl32_4])],[avatar_definition]) ).
fof(f5773,plain,
( l1_vectsp_2(sK3,sK2)
| ~ spl32_4 ),
inference(avatar_component_clause,[],[f5771]) ).
fof(f5774,plain,
spl32_4,
inference(avatar_split_clause,[],[f3622,f5771]) ).
fof(f5780,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| ~ spl32_4 ),
inference(resolution,[],[f5773,f3611]) ).
fof(f5890,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f5780,f3807]) ).
fof(f5949,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f5890,f3627]) ).
fof(f6008,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f5949,f3626]) ).
fof(f6067,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6008,f3625]) ).
fof(f6126,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6067,f3624]) ).
fof(f6185,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6126,f3623]) ).
fof(f6244,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6185,f3812]) ).
fof(f6303,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6244,f3620]) ).
fof(f6362,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6303,f3619]) ).
fof(f6421,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6362,f3618]) ).
fof(f6480,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6421,f3617]) ).
fof(f6539,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6480,f3616]) ).
fof(f6598,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6539,f3615]) ).
fof(f6657,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6598,f3614]) ).
fof(f6716,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6657,f3613]) ).
fof(f6775,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) )
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f6716,f3612]) ).
fof(f6803,definition,
( spl32_5
<=> ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) ) ),
introduced(definition,[new_symbols(definition,[spl32_5])],[avatar_definition]) ).
fof(f6804,plain,
( ! [X0] :
( k1_xboole_0 != k2_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) )
| ~ spl32_5 ),
inference(avatar_component_clause,[],[f6803]) ).
fof(f6805,plain,
( spl32_5
| spl32_1
| spl32_2
| ~ spl32_4 ),
inference(avatar_split_clause,[],[f6775,f5771,f3810,f3805,f6803]) ).
fof(f6806,plain,
( ! [X0,X1] :
( k1_xboole_0 != k1_xboole_0
| v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| k1_rlvect_1(sK3) != k5_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| ~ spl32_5 ),
inference(superposition,[],[f6804,f3608]) ).
fof(f6807,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| k1_rlvect_1(sK3) != k5_rmod_4(sK2,sK3,sK1(sK2,sK3,X0))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| ~ spl32_5 ),
inference(trivial_inequality_removal,[],[f6806]) ).
fof(f6808,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_2
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6807,f5742]) ).
fof(f6809,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6808,f3807]) ).
fof(f6810,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6809,f3627]) ).
fof(f6811,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6810,f3626]) ).
fof(f6812,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6811,f3625]) ).
fof(f6813,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6812,f3624]) ).
fof(f6814,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6813,f3623]) ).
fof(f6815,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6814,f5773]) ).
fof(f6816,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6815,f3812]) ).
fof(f6817,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6816,f3620]) ).
fof(f6818,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6817,f3619]) ).
fof(f6819,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6818,f3618]) ).
fof(f6820,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6819,f3617]) ).
fof(f6821,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6820,f3616]) ).
fof(f6822,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6821,f3615]) ).
fof(f6823,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6822,f3614]) ).
fof(f6824,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6823,f3613]) ).
fof(f6825,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3))) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f6824,f3612]) ).
fof(f6846,definition,
( spl32_6
<=> m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3))) ),
introduced(definition,[new_symbols(definition,[spl32_6])],[avatar_definition]) ).
fof(f6848,plain,
( m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl32_6 ),
inference(avatar_component_clause,[],[f6846]) ).
fof(f6849,plain,
spl32_6,
inference(avatar_split_clause,[],[f3629,f6846]) ).
fof(f6947,definition,
( spl32_7
<=> v5_vectsp_2(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl32_7])],[avatar_definition]) ).
fof(f6949,plain,
( v5_vectsp_2(sK3,sK2)
| ~ spl32_7 ),
inference(avatar_component_clause,[],[f6947]) ).
fof(f6950,plain,
spl32_7,
inference(avatar_split_clause,[],[f3623,f6947]) ).
fof(f7055,definition,
( spl32_8
<=> v1_rmod_5(sK4,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition]) ).
fof(f7057,plain,
( ~ v1_rmod_5(sK4,sK2,sK3)
| spl32_8 ),
inference(avatar_component_clause,[],[f7055]) ).
fof(f7058,plain,
~ spl32_8,
inference(avatar_split_clause,[],[f3633,f7055]) ).
fof(f7060,definition,
( spl32_9
<=> ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3))) ) ),
introduced(definition,[new_symbols(definition,[spl32_9])],[avatar_definition]) ).
fof(f7061,plain,
( ! [X0,X1] :
( ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3))) )
| ~ spl32_9 ),
inference(avatar_component_clause,[],[f7060]) ).
fof(f7062,plain,
( spl32_9
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5 ),
inference(avatar_split_clause,[],[f6825,f6803,f5771,f3810,f3805,f7060]) ).
fof(f7066,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| ~ spl32_9 ),
inference(resolution,[],[f7061,f3770]) ).
fof(f7067,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| ~ spl32_9 ),
inference(duplicate_literal_removal,[],[f7066]) ).
fof(f7070,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7067,f3807]) ).
fof(f7073,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7070,f3627]) ).
fof(f7076,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7073,f3626]) ).
fof(f7079,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7076,f3625]) ).
fof(f7082,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7079,f3624]) ).
fof(f7085,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7082,f6949]) ).
fof(f7088,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7085,f5773]) ).
fof(f7091,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7088,f3812]) ).
fof(f7094,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7091,f3620]) ).
fof(f7097,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7094,f3619]) ).
fof(f7100,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7097,f3618]) ).
fof(f7103,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7100,f3617]) ).
fof(f7106,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7103,f3616]) ).
fof(f7109,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7106,f3615]) ).
fof(f7112,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7109,f3614]) ).
fof(f7115,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7112,f3613]) ).
fof(f7118,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3))) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(forward_subsumption_resolution,[],[f7115,f3612]) ).
fof(f7127,definition,
( spl32_11
<=> v5_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl32_11])],[avatar_definition]) ).
fof(f7129,plain,
( v5_rlvect_1(sK3)
| ~ spl32_11 ),
inference(avatar_component_clause,[],[f7127]) ).
fof(f7130,plain,
spl32_11,
inference(avatar_split_clause,[],[f3625,f7127]) ).
fof(f7132,definition,
( spl32_12
<=> v3_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl32_12])],[avatar_definition]) ).
fof(f7134,plain,
( v3_rlvect_1(sK3)
| ~ spl32_12 ),
inference(avatar_component_clause,[],[f7132]) ).
fof(f7135,plain,
spl32_12,
inference(avatar_split_clause,[],[f3627,f7132]) ).
fof(f7137,definition,
( spl32_13
<=> v6_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl32_13])],[avatar_definition]) ).
fof(f7139,plain,
( v6_rlvect_1(sK3)
| ~ spl32_13 ),
inference(avatar_component_clause,[],[f7137]) ).
fof(f7140,plain,
spl32_13,
inference(avatar_split_clause,[],[f3624,f7137]) ).
fof(f7199,definition,
( spl32_14
<=> v8_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_14])],[avatar_definition]) ).
fof(f7201,plain,
( v8_vectsp_1(sK2)
| ~ spl32_14 ),
inference(avatar_component_clause,[],[f7199]) ).
fof(f7202,plain,
spl32_14,
inference(avatar_split_clause,[],[f3613,f7199]) ).
fof(f7221,definition,
( spl32_15
<=> v4_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl32_15])],[avatar_definition]) ).
fof(f7223,plain,
( v4_rlvect_1(sK3)
| ~ spl32_15 ),
inference(avatar_component_clause,[],[f7221]) ).
fof(f7224,plain,
spl32_15,
inference(avatar_split_clause,[],[f3626,f7221]) ).
fof(f7226,definition,
( spl32_16
<=> l3_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_16])],[avatar_definition]) ).
fof(f7228,plain,
( l3_vectsp_1(sK2)
| ~ spl32_16 ),
inference(avatar_component_clause,[],[f7226]) ).
fof(f7229,plain,
spl32_16,
inference(avatar_split_clause,[],[f3612,f7226]) ).
fof(f7231,definition,
( spl32_17
<=> v5_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_17])],[avatar_definition]) ).
fof(f7233,plain,
( v5_rlvect_1(sK2)
| ~ spl32_17 ),
inference(avatar_component_clause,[],[f7231]) ).
fof(f7234,plain,
spl32_17,
inference(avatar_split_clause,[],[f3618,f7231]) ).
fof(f7404,definition,
( spl32_18
<=> v3_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_18])],[avatar_definition]) ).
fof(f7406,plain,
( v3_rlvect_1(sK2)
| ~ spl32_18 ),
inference(avatar_component_clause,[],[f7404]) ).
fof(f7407,plain,
spl32_18,
inference(avatar_split_clause,[],[f3620,f7404]) ).
fof(f7715,definition,
( spl32_19
<=> v7_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_19])],[avatar_definition]) ).
fof(f7717,plain,
( v7_vectsp_1(sK2)
| ~ spl32_19 ),
inference(avatar_component_clause,[],[f7715]) ).
fof(f7718,plain,
spl32_19,
inference(avatar_split_clause,[],[f3614,f7715]) ).
fof(f7819,definition,
( spl32_20
<=> v6_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_20])],[avatar_definition]) ).
fof(f7821,plain,
( v6_rlvect_1(sK2)
| ~ spl32_20 ),
inference(avatar_component_clause,[],[f7819]) ).
fof(f7822,plain,
spl32_20,
inference(avatar_split_clause,[],[f3617,f7819]) ).
fof(f7977,definition,
( spl32_21
<=> v4_group_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_21])],[avatar_definition]) ).
fof(f7979,plain,
( v4_group_1(sK2)
| ~ spl32_21 ),
inference(avatar_component_clause,[],[f7977]) ).
fof(f7980,plain,
spl32_21,
inference(avatar_split_clause,[],[f3616,f7977]) ).
fof(f8447,definition,
( spl32_22
<=> r1_tarski(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl32_22])],[avatar_definition]) ).
fof(f8449,plain,
( r1_tarski(sK4,sK5)
| ~ spl32_22 ),
inference(avatar_component_clause,[],[f8447]) ).
fof(f8450,plain,
spl32_22,
inference(avatar_split_clause,[],[f3632,f8447]) ).
fof(f8550,definition,
( spl32_23
<=> v4_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_23])],[avatar_definition]) ).
fof(f8552,plain,
( v4_rlvect_1(sK2)
| ~ spl32_23 ),
inference(avatar_component_clause,[],[f8550]) ).
fof(f8553,plain,
spl32_23,
inference(avatar_split_clause,[],[f3619,f8550]) ).
fof(f8976,definition,
( spl32_28
<=> v6_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_28])],[avatar_definition]) ).
fof(f8978,plain,
( v6_vectsp_1(sK2)
| ~ spl32_28 ),
inference(avatar_component_clause,[],[f8976]) ).
fof(f8979,plain,
spl32_28,
inference(avatar_split_clause,[],[f3615,f8976]) ).
fof(f8981,definition,
( spl32_29
<=> m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK3))) ),
introduced(definition,[new_symbols(definition,[spl32_29])],[avatar_definition]) ).
fof(f8983,plain,
( m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl32_29 ),
inference(avatar_component_clause,[],[f8981]) ).
fof(f8984,plain,
spl32_29,
inference(avatar_split_clause,[],[f3630,f8981]) ).
fof(f9208,definition,
( spl32_34
<=> ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3))) ) ),
introduced(definition,[new_symbols(definition,[spl32_34])],[avatar_definition]) ).
fof(f9209,plain,
( ! [X2,X0,X1] :
( ~ m2_rmod_4(sK1(sK2,sK3,X0),sK2,sK3,X2)
| v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X2,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK3))) )
| ~ spl32_34 ),
inference(avatar_component_clause,[],[f9208]) ).
fof(f9210,plain,
( spl32_34
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9 ),
inference(avatar_split_clause,[],[f7118,f7060,f6947,f5771,f3810,f3805,f9208]) ).
fof(f9211,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v1_rmod_5(X0,sK2,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| ~ spl32_34 ),
inference(resolution,[],[f9209,f3609]) ).
fof(f9217,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| ~ spl32_34 ),
inference(duplicate_literal_removal,[],[f9211]) ).
fof(f9220,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9217,f3807]) ).
fof(f9222,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_12
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9220,f7134]) ).
fof(f9224,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_12
| ~ spl32_15
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9222,f7223]) ).
fof(f9226,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_11
| ~ spl32_12
| ~ spl32_15
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9224,f7129]) ).
fof(f9228,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9226,f7139]) ).
fof(f9230,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9228,f6949]) ).
fof(f9232,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9230,f5773]) ).
fof(f9234,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9232,f3812]) ).
fof(f9236,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_18
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9234,f7406]) ).
fof(f9238,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_18
| ~ spl32_23
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9236,f8552]) ).
fof(f9240,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_17
| ~ spl32_18
| ~ spl32_23
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9238,f7233]) ).
fof(f9242,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_17
| ~ spl32_18
| ~ spl32_20
| ~ spl32_23
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9240,f7821]) ).
fof(f9244,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_17
| ~ spl32_18
| ~ spl32_20
| ~ spl32_21
| ~ spl32_23
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9242,f7979]) ).
fof(f9246,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_17
| ~ spl32_18
| ~ spl32_20
| ~ spl32_21
| ~ spl32_23
| ~ spl32_28
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9244,f8978]) ).
fof(f9248,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_15
| ~ spl32_17
| ~ spl32_18
| ~ spl32_19
| ~ spl32_20
| ~ spl32_21
| ~ spl32_23
| ~ spl32_28
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9246,f7717]) ).
fof(f9250,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l3_vectsp_1(sK2) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_14
| ~ spl32_15
| ~ spl32_17
| ~ spl32_18
| ~ spl32_19
| ~ spl32_20
| ~ spl32_21
| ~ spl32_23
| ~ spl32_28
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9248,f7201]) ).
fof(f9252,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) )
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_14
| ~ spl32_15
| ~ spl32_16
| ~ spl32_17
| ~ spl32_18
| ~ spl32_19
| ~ spl32_20
| ~ spl32_21
| ~ spl32_23
| ~ spl32_28
| ~ spl32_34 ),
inference(forward_subsumption_resolution,[],[f9250,f7228]) ).
fof(f9254,definition,
( spl32_35
<=> ! [X0,X1] :
( v1_rmod_5(X0,sK2,sK3)
| ~ v1_rmod_5(X1,sK2,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) ) ),
introduced(definition,[new_symbols(definition,[spl32_35])],[avatar_definition]) ).
fof(f9255,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v1_rmod_5(X1,sK2,sK3)
| v1_rmod_5(X0,sK2,sK3)
| ~ r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) )
| ~ spl32_35 ),
inference(avatar_component_clause,[],[f9254]) ).
fof(f9256,plain,
( spl32_35
| spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_14
| ~ spl32_15
| ~ spl32_16
| ~ spl32_17
| ~ spl32_18
| ~ spl32_19
| ~ spl32_20
| ~ spl32_21
| ~ spl32_23
| ~ spl32_28
| ~ spl32_34 ),
inference(avatar_split_clause,[],[f9252,f9208,f8976,f8550,f7977,f7819,f7715,f7404,f7231,f7226,f7221,f7199,f7137,f7132,f7127,f6947,f5771,f3810,f3805,f9254]) ).
fof(f9262,plain,
( ! [X0] :
( ~ v1_rmod_5(sK5,sK2,sK3)
| v1_rmod_5(X0,sK2,sK3)
| ~ r1_tarski(X0,sK5)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) )
| ~ spl32_29
| ~ spl32_35 ),
inference(resolution,[],[f9255,f8983]) ).
fof(f9271,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| ~ r1_tarski(X0,sK5)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) )
| ~ spl32_3
| ~ spl32_29
| ~ spl32_35 ),
inference(forward_subsumption_resolution,[],[f9262,f5768]) ).
fof(f9278,definition,
( spl32_36
<=> ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| ~ r1_tarski(X0,sK5)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) ) ),
introduced(definition,[new_symbols(definition,[spl32_36])],[avatar_definition]) ).
fof(f9279,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,sK5)
| v1_rmod_5(X0,sK2,sK3) )
| ~ spl32_36 ),
inference(avatar_component_clause,[],[f9278]) ).
fof(f9280,plain,
( spl32_36
| ~ spl32_3
| ~ spl32_29
| ~ spl32_35 ),
inference(avatar_split_clause,[],[f9271,f9254,f8981,f5766,f9278]) ).
fof(f9285,plain,
( ~ r1_tarski(sK4,sK5)
| v1_rmod_5(sK4,sK2,sK3)
| ~ spl32_6
| ~ spl32_36 ),
inference(resolution,[],[f9279,f6848]) ).
fof(f9295,plain,
( v1_rmod_5(sK4,sK2,sK3)
| ~ spl32_6
| ~ spl32_22
| ~ spl32_36 ),
inference(forward_subsumption_resolution,[],[f9285,f8449]) ).
fof(f9298,plain,
( $false
| ~ spl32_6
| spl32_8
| ~ spl32_22
| ~ spl32_36 ),
inference(forward_subsumption_resolution,[],[f9295,f7057]) ).
fof(f9299,plain,
( ~ spl32_6
| spl32_8
| ~ spl32_22
| ~ spl32_36 ),
inference(avatar_contradiction_clause,[],[f9298]) ).
cnf(s1,plain,
~ spl32_1,
inference(sat_conversion,[],[f3808]) ).
cnf(s2,plain,
~ spl32_2,
inference(sat_conversion,[],[f3813]) ).
cnf(s3,plain,
spl32_3,
inference(sat_conversion,[],[f5769]) ).
cnf(s4,plain,
spl32_4,
inference(sat_conversion,[],[f5774]) ).
cnf(s5,plain,
( spl32_1
| spl32_2
| ~ spl32_4
| spl32_5 ),
inference(sat_conversion,[],[f6805]) ).
cnf(s6,plain,
spl32_6,
inference(sat_conversion,[],[f6849]) ).
cnf(s7,plain,
spl32_7,
inference(sat_conversion,[],[f6950]) ).
cnf(s8,plain,
~ spl32_8,
inference(sat_conversion,[],[f7058]) ).
cnf(s9,plain,
( spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_5
| spl32_9 ),
inference(sat_conversion,[],[f7062]) ).
cnf(s11,plain,
spl32_11,
inference(sat_conversion,[],[f7130]) ).
cnf(s12,plain,
spl32_12,
inference(sat_conversion,[],[f7135]) ).
cnf(s13,plain,
spl32_13,
inference(sat_conversion,[],[f7140]) ).
cnf(s14,plain,
spl32_14,
inference(sat_conversion,[],[f7202]) ).
cnf(s15,plain,
spl32_15,
inference(sat_conversion,[],[f7224]) ).
cnf(s16,plain,
spl32_16,
inference(sat_conversion,[],[f7229]) ).
cnf(s17,plain,
spl32_17,
inference(sat_conversion,[],[f7234]) ).
cnf(s18,plain,
spl32_18,
inference(sat_conversion,[],[f7407]) ).
cnf(s19,plain,
spl32_19,
inference(sat_conversion,[],[f7718]) ).
cnf(s20,plain,
spl32_20,
inference(sat_conversion,[],[f7822]) ).
cnf(s21,plain,
spl32_21,
inference(sat_conversion,[],[f7980]) ).
cnf(s22,plain,
spl32_22,
inference(sat_conversion,[],[f8450]) ).
cnf(s23,plain,
spl32_23,
inference(sat_conversion,[],[f8553]) ).
cnf(s27,plain,
spl32_28,
inference(sat_conversion,[],[f8979]) ).
cnf(s28,plain,
spl32_29,
inference(sat_conversion,[],[f8984]) ).
cnf(s33,plain,
( spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_9
| spl32_34 ),
inference(sat_conversion,[],[f9210]) ).
cnf(s34,plain,
( spl32_1
| spl32_2
| ~ spl32_4
| ~ spl32_7
| ~ spl32_11
| ~ spl32_12
| ~ spl32_13
| ~ spl32_14
| ~ spl32_15
| ~ spl32_16
| ~ spl32_17
| ~ spl32_18
| ~ spl32_19
| ~ spl32_20
| ~ spl32_21
| ~ spl32_23
| ~ spl32_28
| ~ spl32_34
| spl32_35 ),
inference(sat_conversion,[],[f9256]) ).
cnf(s35,plain,
( ~ spl32_3
| ~ spl32_29
| ~ spl32_35
| spl32_36 ),
inference(sat_conversion,[],[f9280]) ).
cnf(s36,plain,
( ~ spl32_6
| spl32_8
| ~ spl32_22
| ~ spl32_36 ),
inference(sat_conversion,[],[f9299]) ).
cnf(s37,plain,
~ spl32_36,
inference(rat,[],[s36,s8,s22,s6]) ).
cnf(s38,plain,
~ spl32_35,
inference(rat,[],[s35,s37,s28,s3]) ).
cnf(s40,plain,
~ spl32_34,
inference(rat,[],[s34,s38,s2,s27,s23,s21,s20,s19,s18,s17,s16,s15,s14,s13,s12,s11,s7,s4,s1]) ).
cnf(s41,plain,
~ spl32_9,
inference(rat,[],[s33,s40,s2,s7,s4,s1]) ).
cnf(s45,plain,
~ spl32_5,
inference(rat,[],[s9,s41,s2,s4,s1]) ).
cnf(s46,plain,
$false,
inference(rat,[],[s5,s2,s4,s45,s1]) ).
fof(f9305,plain,
$false,
inference(avatar_sat_refutation,[],[s46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG214+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n013.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 19:43:03 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.59/1.94 % (1486881)Detected formulas, will run a generic FOF schedule.
% 9.59/1.94 % (1486892)dis-21_1_sil=8000:lcm=predicate:random_seed=1840051339: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)
% 9.59/1.94 % (1486890)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2829579642:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.59/1.94 % (1486891)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3065178399:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.59/1.94 % (1486889)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1039941624:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.59/1.94 % (1486888)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=479981084:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.59/1.94 % (1486886)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=440416850:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.59/1.94 % (1486887)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=3763704371:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.59/1.94 % (1486892)Instruction limit reached!
% 9.59/1.94 % (1486892)------------------------------
% 9.59/1.94 % (1486892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/1.94 % (1486892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/1.94 % (1486892)CaDiCaL version: 2.1.3
% 9.59/1.94 % (1486892)Termination reason: Instruction limit
% 9.59/1.94 % (1486892)Termination phase: Property scanning
% 9.59/1.94 % (1486892)Time elapsed: 0.046 s
% 9.59/1.94 % (1486892)Peak memory usage: 94 MB
% 9.59/1.94 % (1486892)Instructions burned: 130 (million)
% 9.59/1.94 % (1486889)Instruction limit reached!
% 9.59/1.94 % (1486889)------------------------------
% 9.59/1.94 % (1486889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/1.94 % (1486889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/1.94 % (1486889)CaDiCaL version: 2.1.3
% 9.59/1.94 % (1486889)Termination reason: Instruction limit
% 9.59/1.94 % (1486889)Termination phase: Saturation
% 9.59/1.94 % (1486889)Time elapsed: 0.065 s
% 9.59/1.94 % (1486889)Peak memory usage: 93 MB
% 9.59/1.94 % (1486889)Instructions burned: 109 (million)
% 9.59/1.94 % (1486890)Instruction limit reached!
% 9.59/1.94 % (1486890)------------------------------
% 9.59/1.94 % (1486890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/1.94 % (1486890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/1.94 % (1486890)CaDiCaL version: 2.1.3
% 9.59/1.94 % (1486890)Termination reason: Instruction limit
% 9.59/1.94 % (1486890)Termination phase: Saturation
% 9.59/1.94 % (1486890)Time elapsed: 0.081 s
% 9.59/1.94 % (1486890)Peak memory usage: 93 MB
% 9.59/1.94 % (1486890)Instructions burned: 120 (million)
% 9.59/1.94 % (1486891)Instruction limit reached!
% 9.59/1.94 % (1486891)------------------------------
% 9.59/1.94 % (1486891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/1.94 % (1486891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/1.94 % (1486891)CaDiCaL version: 2.1.3
% 9.59/1.94 % (1486891)Termination reason: Instruction limit
% 9.59/1.94 % (1486891)Termination phase: Preprocessing 3
% 9.59/1.94 % (1486891)Time elapsed: 0.085 s
% 9.59/1.94 % (1486891)Peak memory usage: 94 MB
% 9.59/1.94 % (1486891)Instructions burned: 140 (million)
% 9.59/1.94 % (1486900)lrs+10_1_sil=8000:sp=occurrence:random_seed=1922999034:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.59/1.94 % (1486901)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3937234512:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.59/1.94 % (1486903)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=2070646368:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 9.59/1.94 % (1486902)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4160235863:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 9.59/1.94 % (1486900)Instruction limit reached!
% 4.46/2.05 % (1486900)------------------------------
% 4.46/2.05 % (1486900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486900)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486900)Termination reason: Instruction limit
% 4.46/2.05 % (1486900)Termination phase: Saturation
% 4.46/2.05 % (1486900)Time elapsed: 0.097 s
% 4.46/2.05 % (1486900)Peak memory usage: 96 MB
% 4.46/2.05 % (1486900)Instructions burned: 288 (million)
% 4.46/2.05 % (1486901)Instruction limit reached!
% 4.46/2.05 % (1486901)------------------------------
% 4.46/2.05 % (1486901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486901)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486901)Termination reason: Instruction limit
% 4.46/2.05 % (1486901)Termination phase: Saturation
% 4.46/2.05 % (1486901)Time elapsed: 0.089 s
% 4.46/2.05 % (1486901)Peak memory usage: 93 MB
% 4.46/2.05 % (1486901)Instructions burned: 158 (million)
% 4.46/2.05 % (1486908)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3091086300:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 4.46/2.05 % (1486903)Instruction limit reached!
% 4.46/2.05 % (1486903)------------------------------
% 4.46/2.05 % (1486903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486903)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486903)Termination reason: Instruction limit
% 4.46/2.05 % (1486903)Termination phase: Function definition elimination
% 4.46/2.05 % (1486903)Time elapsed: 0.138 s
% 4.46/2.05 % (1486903)Peak memory usage: 96 MB
% 4.46/2.05 % (1486903)Instructions burned: 248 (million)
% 4.46/2.05 % (1486909)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2250888478:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 4.46/2.05 % (1486908)Instruction limit reached!
% 4.46/2.05 % (1486908)------------------------------
% 4.46/2.05 % (1486908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486908)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486908)Termination reason: Instruction limit
% 4.46/2.05 % (1486908)Termination phase: Saturation
% 4.46/2.05 % (1486908)Time elapsed: 0.085 s
% 4.46/2.05 % (1486908)Peak memory usage: 96 MB
% 4.46/2.05 % (1486908)Instructions burned: 296 (million)
% 4.46/2.05 % (1486902)Instruction limit reached!
% 4.46/2.05 % (1486902)------------------------------
% 4.46/2.05 % (1486902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486902)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486902)Termination reason: Instruction limit
% 4.46/2.05 % (1486902)Termination phase: Saturation
% 4.46/2.05 % (1486902)Time elapsed: 0.230 s
% 4.46/2.05 % (1486902)Peak memory usage: 95 MB
% 4.46/2.05 % (1486902)Instructions burned: 325 (million)
% 4.46/2.05 % (1486911)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2033737380:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 4.46/2.05 % (1486913)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4130117492:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 4.46/2.05 % (1486913)Instruction limit reached!
% 4.46/2.05 % (1486913)------------------------------
% 4.46/2.05 % (1486913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486913)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486913)Termination reason: Instruction limit
% 4.46/2.05 % (1486913)Termination phase: Property scanning
% 4.46/2.05 % (1486913)Time elapsed: 0.046 s
% 4.46/2.05 % (1486913)Peak memory usage: 96 MB
% 4.46/2.05 % (1486913)Instructions burned: 129 (million)
% 4.46/2.05 % (1486911)Instruction limit reached!
% 4.46/2.05 % (1486911)------------------------------
% 4.46/2.05 % (1486911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486911)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486911)Termination reason: Instruction limit
% 4.46/2.05 % (1486911)Termination phase: Saturation
% 4.46/2.05 % (1486911)Time elapsed: 0.068 s
% 4.46/2.05 % (1486911)Peak memory usage: 94 MB
% 4.46/2.05 % (1486911)Instructions burned: 113 (million)
% 4.46/2.05 % (1486914)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1043621858:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 4.46/2.05 % (1486914)Instruction limit reached!
% 4.46/2.05 % (1486914)------------------------------
% 4.46/2.05 % (1486914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486914)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486914)Termination reason: Instruction limit
% 4.46/2.05 % (1486914)Termination phase: Preprocessing 3
% 4.46/2.05 % (1486914)Time elapsed: 0.059 s
% 4.46/2.05 % (1486914)Peak memory usage: 91 MB
% 4.46/2.05 % (1486914)Instructions burned: 114 (million)
% 4.46/2.05 % (1486917)lrs+10_1_sil=8000:sp=occurrence:random_seed=673989378:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 4.46/2.05 % (1486918)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=768704549:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 4.46/2.05 % (1486921)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3770840889:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 4.46/2.05 % (1486918)Instruction limit reached!
% 4.46/2.05 % (1486918)------------------------------
% 4.46/2.05 % (1486918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486918)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486918)Termination reason: Instruction limit
% 4.46/2.05 % (1486918)Termination phase: Saturation
% 4.46/2.05 % (1486918)Time elapsed: 0.254 s
% 4.46/2.05 % (1486918)Peak memory usage: 95 MB
% 4.46/2.05 % (1486918)Instructions burned: 438 (million)
% 4.46/2.05 % (1486917)Instruction limit reached!
% 4.46/2.05 % (1486917)------------------------------
% 4.46/2.05 % (1486917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486917)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486917)Termination reason: Instruction limit
% 4.46/2.05 % (1486917)Termination phase: Saturation
% 4.46/2.05 % (1486917)Time elapsed: 0.331 s
% 4.46/2.05 % (1486917)Peak memory usage: 103 MB
% 4.46/2.05 % (1486917)Instructions burned: 907 (million)
% 4.46/2.05 % (1486925)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=683043574:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 4.46/2.05 % (1486924)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1227993134:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 4.46/2.05 % (1486888)First to succeed.
% 4.46/2.05 % (1486924)Instruction limit reached!
% 4.46/2.05 % (1486924)------------------------------
% 4.46/2.05 % (1486924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486924)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486924)Termination reason: Instruction limit
% 4.46/2.05 % (1486924)Termination phase: Saturation
% 4.46/2.05 % (1486924)Time elapsed: 0.084 s
% 4.46/2.05 % (1486924)Peak memory usage: 95 MB
% 4.46/2.05 % (1486924)Instructions burned: 134 (million)
% 4.46/2.05 % (1486888)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1486881"
% 4.46/2.05 % (1486925)Instruction limit reached!
% 4.46/2.05 % (1486925)------------------------------
% 4.46/2.05 % (1486925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486925)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486925)Termination reason: Instruction limit
% 4.46/2.05 % (1486925)Termination phase: Saturation
% 4.46/2.05 % (1486925)Time elapsed: 0.170 s
% 4.46/2.05 % (1486925)Peak memory usage: 105 MB
% 4.46/2.05 % (1486925)Instructions burned: 594 (million)
% 4.46/2.05 % (1486928)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2456885062:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 4.46/2.05 % (1486929)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=2236063435:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 4.46/2.05 % (1486929)Instruction limit reached!
% 4.46/2.05 % (1486929)------------------------------
% 4.46/2.05 % (1486929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.46/2.05 % (1486929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.46/2.05 % (1486929)CaDiCaL version: 2.1.3
% 4.46/2.05 % (1486929)Termination reason: Instruction limit
% 4.46/2.05 % (1486929)Termination phase: Saturation
% 4.46/2.05 % (1486929)Time elapsed: 0.039 s
% 4.46/2.05 % (1486929)Peak memory usage: 93 MB
% 4.46/2.05 % (1486929)Instructions burned: 128 (million)
% 4.46/2.05 % (1486887)Also succeeded, but the first one will report.
% 4.46/2.05 % (1486888)Refutation found. Thanks to Tanya!
% 4.46/2.05 % SZS status Theorem for theBenchmark
% 4.46/2.05 % SZS output start Proof for theBenchmark
% See solution above
% 11.66/2.25 % (1486888)------------------------------
% 11.66/2.25 % (1486888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.66/2.25 % (1486888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.66/2.25 % (1486888)CaDiCaL version: 2.1.3
% 11.66/2.25 % (1486888)Termination reason: Refutation
% 11.66/2.25 % (1486888)Time elapsed: 1.183 s
% 11.66/2.25 % (1486888)Peak memory usage: 141 MB
% 11.66/2.25 % (1486888)Instructions burned: 1977 (million)
% 11.66/2.25 % (1486888)------------------------------
% 11.66/2.25 % (1486888)------------------------------
% 11.66/2.25 % (1486881)Success in time 1.648 s
% 11.66/2.25 % Vampire exiting
%------------------------------------------------------------------------------