%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG214+3 : 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 : n004.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.56s 2.78s
% Output : Refutation 12.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 30
% Syntax : Number of formulae : 243 ( 73 unt; 27 def)
% Number of atoms : 2382 ( 49 equ)
% Maximal formula atoms : 26 ( 9 avg)
% Number of connectives : 3915 (1776 ~;1954 |; 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 : 257 ( 0 sgn 247 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9907,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(f9990,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(f9992,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(f9993,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)],[f9992]) ).
fof(f10012,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,[],[f9990]) ).
fof(f10013,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,[],[f10012]) ).
fof(f10014,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,[],[f9993]) ).
fof(f10015,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,[],[f10014]) ).
fof(f10116,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,[],[f9907]) ).
fof(f10117,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,[],[f10116]) ).
fof(f10145,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,[],[f10013]) ).
fof(f10146,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,[],[f10145]) ).
fof(f10147,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))],[f10146]) ).
fof(f10148,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)],[f10015]) ).
fof(f10202,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,[],[f10147]) ).
fof(f10203,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,[],[f10147]) ).
fof(f10204,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,[],[f10147]) ).
fof(f10205,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,[],[f10147]) ).
fof(f10206,plain,
l3_vectsp_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10207,plain,
v8_vectsp_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10208,plain,
v7_vectsp_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10209,plain,
v6_vectsp_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10210,plain,
v4_group_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10211,plain,
v6_rlvect_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10212,plain,
v5_rlvect_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10213,plain,
v4_rlvect_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10214,plain,
v3_rlvect_1(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10215,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10216,plain,
l1_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10217,plain,
v5_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f10148]) ).
fof(f10218,plain,
v6_rlvect_1(sK3),
inference(cnf_transformation,[],[f10148]) ).
fof(f10219,plain,
v5_rlvect_1(sK3),
inference(cnf_transformation,[],[f10148]) ).
fof(f10220,plain,
v4_rlvect_1(sK3),
inference(cnf_transformation,[],[f10148]) ).
fof(f10221,plain,
v3_rlvect_1(sK3),
inference(cnf_transformation,[],[f10148]) ).
fof(f10222,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f10148]) ).
fof(f10223,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3))),
inference(cnf_transformation,[],[f10148]) ).
fof(f10224,plain,
m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK3))),
inference(cnf_transformation,[],[f10148]) ).
fof(f10225,plain,
v1_rmod_5(sK5,sK2,sK3),
inference(cnf_transformation,[],[f10148]) ).
fof(f10226,plain,
r1_tarski(sK4,sK5),
inference(cnf_transformation,[],[f10148]) ).
fof(f10227,plain,
~ v1_rmod_5(sK4,sK2,sK3),
inference(cnf_transformation,[],[f10148]) ).
fof(f10392,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,[],[f10117]) ).
fof(f10460,definition,
( spl45_1
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl45_1])],[avatar_definition]) ).
fof(f10462,plain,
( ~ v3_struct_0(sK3)
| spl45_1 ),
inference(avatar_component_clause,[],[f10460]) ).
fof(f10463,plain,
~ spl45_1,
inference(avatar_split_clause,[],[f10222,f10460]) ).
fof(f10465,definition,
( spl45_2
<=> v3_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_2])],[avatar_definition]) ).
fof(f10467,plain,
( ~ v3_struct_0(sK2)
| spl45_2 ),
inference(avatar_component_clause,[],[f10465]) ).
fof(f10468,plain,
~ spl45_2,
inference(avatar_split_clause,[],[f10215,f10465]) ).
fof(f11793,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,X1,sK3)
| k1_rlvect_1(sK3) = k5_rmod_4(X1,sK3,sK1(X1,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,X1)
| ~ l1_vectsp_2(sK3,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1) )
| spl45_1 ),
inference(resolution,[],[f10462,f10204]) ).
fof(f12108,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,X1,sK3)
| k1_rlvect_1(sK3) = k5_rmod_4(X1,sK3,sK1(X1,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,X1)
| ~ l1_vectsp_2(sK3,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1) )
| spl45_1 ),
inference(forward_subsumption_resolution,[],[f11793,f10221]) ).
fof(f12273,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,X1,sK3)
| k1_rlvect_1(sK3) = k5_rmod_4(X1,sK3,sK1(X1,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,X1)
| ~ l1_vectsp_2(sK3,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1) )
| spl45_1 ),
inference(forward_subsumption_resolution,[],[f12108,f10220]) ).
fof(f12438,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,X1,sK3)
| k1_rlvect_1(sK3) = k5_rmod_4(X1,sK3,sK1(X1,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,X1)
| ~ l1_vectsp_2(sK3,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1) )
| spl45_1 ),
inference(forward_subsumption_resolution,[],[f12273,f10219]) ).
fof(f12601,plain,
( ! [X0,X1] :
( v1_rmod_5(X0,X1,sK3)
| k1_rlvect_1(sK3) = k5_rmod_4(X1,sK3,sK1(X1,sK3,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_vectsp_2(sK3,X1)
| ~ l1_vectsp_2(sK3,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1) )
| spl45_1 ),
inference(forward_subsumption_resolution,[],[f12438,f10218]) ).
fof(f12646,definition,
( spl45_3
<=> l1_vectsp_2(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl45_3])],[avatar_definition]) ).
fof(f12648,plain,
( l1_vectsp_2(sK3,sK2)
| ~ spl45_3 ),
inference(avatar_component_clause,[],[f12646]) ).
fof(f12649,plain,
spl45_3,
inference(avatar_split_clause,[],[f10216,f12646]) ).
fof(f12655,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) )
| ~ spl45_3 ),
inference(resolution,[],[f12648,f10205]) ).
fof(f12783,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) )
| spl45_1
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f12655,f10462]) ).
fof(f12851,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) )
| spl45_1
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f12783,f10221]) ).
fof(f12919,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) )
| spl45_1
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f12851,f10220]) ).
fof(f12987,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) )
| spl45_1
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f12919,f10219]) ).
fof(f13055,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) )
| spl45_1
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f12987,f10218]) ).
fof(f13123,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) )
| spl45_1
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13055,f10217]) ).
fof(f13191,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13123,f10467]) ).
fof(f13259,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13191,f10214]) ).
fof(f13327,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13259,f10213]) ).
fof(f13395,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13327,f10212]) ).
fof(f13463,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13395,f10211]) ).
fof(f13531,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13463,f10210]) ).
fof(f13599,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13531,f10209]) ).
fof(f13667,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13599,f10208]) ).
fof(f13735,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) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13667,f10207]) ).
fof(f13803,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))) )
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(forward_subsumption_resolution,[],[f13735,f10206]) ).
fof(f13831,definition,
( spl45_4
<=> m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3))) ),
introduced(definition,[new_symbols(definition,[spl45_4])],[avatar_definition]) ).
fof(f13833,plain,
( m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl45_4 ),
inference(avatar_component_clause,[],[f13831]) ).
fof(f13834,plain,
spl45_4,
inference(avatar_split_clause,[],[f10223,f13831]) ).
fof(f13933,definition,
( spl45_5
<=> v1_rmod_5(sK5,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl45_5])],[avatar_definition]) ).
fof(f13935,plain,
( v1_rmod_5(sK5,sK2,sK3)
| ~ spl45_5 ),
inference(avatar_component_clause,[],[f13933]) ).
fof(f13936,plain,
spl45_5,
inference(avatar_split_clause,[],[f10225,f13933]) ).
fof(f13938,definition,
( spl45_6
<=> v5_vectsp_2(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl45_6])],[avatar_definition]) ).
fof(f13940,plain,
( v5_vectsp_2(sK3,sK2)
| ~ spl45_6 ),
inference(avatar_component_clause,[],[f13938]) ).
fof(f13941,plain,
spl45_6,
inference(avatar_split_clause,[],[f10217,f13938]) ).
fof(f14047,definition,
( spl45_7
<=> l3_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_7])],[avatar_definition]) ).
fof(f14049,plain,
( l3_vectsp_1(sK2)
| ~ spl45_7 ),
inference(avatar_component_clause,[],[f14047]) ).
fof(f14050,plain,
spl45_7,
inference(avatar_split_clause,[],[f10206,f14047]) ).
fof(f14052,definition,
( spl45_8
<=> v8_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_8])],[avatar_definition]) ).
fof(f14054,plain,
( v8_vectsp_1(sK2)
| ~ spl45_8 ),
inference(avatar_component_clause,[],[f14052]) ).
fof(f14055,plain,
spl45_8,
inference(avatar_split_clause,[],[f10207,f14052]) ).
fof(f14057,definition,
( spl45_9
<=> v4_group_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_9])],[avatar_definition]) ).
fof(f14059,plain,
( v4_group_1(sK2)
| ~ spl45_9 ),
inference(avatar_component_clause,[],[f14057]) ).
fof(f14060,plain,
spl45_9,
inference(avatar_split_clause,[],[f10210,f14057]) ).
fof(f14062,definition,
( spl45_10
<=> v7_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_10])],[avatar_definition]) ).
fof(f14064,plain,
( v7_vectsp_1(sK2)
| ~ spl45_10 ),
inference(avatar_component_clause,[],[f14062]) ).
fof(f14065,plain,
spl45_10,
inference(avatar_split_clause,[],[f10208,f14062]) ).
fof(f14067,definition,
( spl45_11
<=> v3_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl45_11])],[avatar_definition]) ).
fof(f14069,plain,
( v3_rlvect_1(sK3)
| ~ spl45_11 ),
inference(avatar_component_clause,[],[f14067]) ).
fof(f14070,plain,
spl45_11,
inference(avatar_split_clause,[],[f10221,f14067]) ).
fof(f14072,definition,
( spl45_12
<=> v5_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl45_12])],[avatar_definition]) ).
fof(f14074,plain,
( v5_rlvect_1(sK3)
| ~ spl45_12 ),
inference(avatar_component_clause,[],[f14072]) ).
fof(f14075,plain,
spl45_12,
inference(avatar_split_clause,[],[f10219,f14072]) ).
fof(f14077,definition,
( spl45_13
<=> v1_rmod_5(sK4,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl45_13])],[avatar_definition]) ).
fof(f14079,plain,
( ~ v1_rmod_5(sK4,sK2,sK3)
| spl45_13 ),
inference(avatar_component_clause,[],[f14077]) ).
fof(f14080,plain,
~ spl45_13,
inference(avatar_split_clause,[],[f10227,f14077]) ).
fof(f14082,definition,
( spl45_14
<=> v6_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl45_14])],[avatar_definition]) ).
fof(f14084,plain,
( v6_rlvect_1(sK3)
| ~ spl45_14 ),
inference(avatar_component_clause,[],[f14082]) ).
fof(f14085,plain,
spl45_14,
inference(avatar_split_clause,[],[f10218,f14082]) ).
fof(f14087,definition,
( spl45_15
<=> ! [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,[spl45_15])],[avatar_definition]) ).
fof(f14088,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))) )
| ~ spl45_15 ),
inference(avatar_component_clause,[],[f14087]) ).
fof(f14089,plain,
( spl45_15
| spl45_1
| spl45_2
| ~ spl45_3 ),
inference(avatar_split_clause,[],[f13803,f12646,f10465,f10460,f14087]) ).
fof(f14090,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) )
| ~ spl45_15 ),
inference(superposition,[],[f14088,f10202]) ).
fof(f14091,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) )
| ~ spl45_15 ),
inference(trivial_inequality_removal,[],[f14090]) ).
fof(f14092,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) )
| spl45_1
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14091,f12601]) ).
fof(f14093,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) )
| spl45_1
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14092,f10462]) ).
fof(f14094,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14093,f14069]) ).
fof(f14095,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14094,f10220]) ).
fof(f14096,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_12
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14095,f14074]) ).
fof(f14097,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14096,f14084]) ).
fof(f14098,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) )
| spl45_1
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14097,f13940]) ).
fof(f14099,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) )
| spl45_1
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14098,f12648]) ).
fof(f14100,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14099,f10467]) ).
fof(f14101,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14100,f10214]) ).
fof(f14102,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14101,f10213]) ).
fof(f14103,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14102,f10212]) ).
fof(f14104,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14103,f10211]) ).
fof(f14105,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14104,f14059]) ).
fof(f14106,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14105,f10209]) ).
fof(f14107,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14106,f14064]) ).
fof(f14108,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14107,f14054]) ).
fof(f14109,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))) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(forward_subsumption_resolution,[],[f14108,f14049]) ).
fof(f14111,definition,
( spl45_16
<=> ! [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,[spl45_16])],[avatar_definition]) ).
fof(f14112,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))) )
| ~ spl45_16 ),
inference(avatar_component_clause,[],[f14111]) ).
fof(f14113,plain,
( spl45_16
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15 ),
inference(avatar_split_clause,[],[f14109,f14087,f14082,f14072,f14067,f14062,f14057,f14052,f14047,f13938,f12646,f10465,f10460,f14111]) ).
fof(f14117,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) )
| ~ spl45_16 ),
inference(resolution,[],[f14112,f10392]) ).
fof(f14118,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) )
| ~ spl45_16 ),
inference(duplicate_literal_removal,[],[f14117]) ).
fof(f14121,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) )
| spl45_1
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14118,f10462]) ).
fof(f14124,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14121,f14069]) ).
fof(f14127,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14124,f10220]) ).
fof(f14130,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_12
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14127,f14074]) ).
fof(f14133,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14130,f14084]) ).
fof(f14136,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) )
| spl45_1
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14133,f13940]) ).
fof(f14139,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) )
| spl45_1
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14136,f12648]) ).
fof(f14142,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14139,f10467]) ).
fof(f14145,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14142,f10214]) ).
fof(f14148,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14145,f10213]) ).
fof(f14151,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14148,f10212]) ).
fof(f14154,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14151,f10211]) ).
fof(f14157,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14154,f14059]) ).
fof(f14160,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14157,f10209]) ).
fof(f14163,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14160,f14064]) ).
fof(f14166,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14163,f14054]) ).
fof(f14169,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))) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(forward_subsumption_resolution,[],[f14166,f14049]) ).
fof(f14178,definition,
( spl45_18
<=> v6_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_18])],[avatar_definition]) ).
fof(f14180,plain,
( v6_vectsp_1(sK2)
| ~ spl45_18 ),
inference(avatar_component_clause,[],[f14178]) ).
fof(f14181,plain,
spl45_18,
inference(avatar_split_clause,[],[f10209,f14178]) ).
fof(f14391,definition,
( spl45_19
<=> v4_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl45_19])],[avatar_definition]) ).
fof(f14393,plain,
( v4_rlvect_1(sK3)
| ~ spl45_19 ),
inference(avatar_component_clause,[],[f14391]) ).
fof(f14394,plain,
spl45_19,
inference(avatar_split_clause,[],[f10220,f14391]) ).
fof(f14651,definition,
( spl45_20
<=> v3_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_20])],[avatar_definition]) ).
fof(f14653,plain,
( v3_rlvect_1(sK2)
| ~ spl45_20 ),
inference(avatar_component_clause,[],[f14651]) ).
fof(f14654,plain,
spl45_20,
inference(avatar_split_clause,[],[f10214,f14651]) ).
fof(f14841,definition,
( spl45_21
<=> v5_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_21])],[avatar_definition]) ).
fof(f14843,plain,
( v5_rlvect_1(sK2)
| ~ spl45_21 ),
inference(avatar_component_clause,[],[f14841]) ).
fof(f14844,plain,
spl45_21,
inference(avatar_split_clause,[],[f10212,f14841]) ).
fof(f15202,definition,
( spl45_22
<=> v6_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_22])],[avatar_definition]) ).
fof(f15204,plain,
( v6_rlvect_1(sK2)
| ~ spl45_22 ),
inference(avatar_component_clause,[],[f15202]) ).
fof(f15205,plain,
spl45_22,
inference(avatar_split_clause,[],[f10211,f15202]) ).
fof(f15207,definition,
( spl45_23
<=> ! [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,[spl45_23])],[avatar_definition]) ).
fof(f15208,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))) )
| ~ spl45_23 ),
inference(avatar_component_clause,[],[f15207]) ).
fof(f15209,plain,
( spl45_23
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16 ),
inference(avatar_split_clause,[],[f14169,f14111,f14082,f14072,f14067,f14062,f14057,f14052,f14047,f13938,f12646,f10465,f10460,f15207]) ).
fof(f16021,definition,
( spl45_24
<=> r1_tarski(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl45_24])],[avatar_definition]) ).
fof(f16023,plain,
( r1_tarski(sK4,sK5)
| ~ spl45_24 ),
inference(avatar_component_clause,[],[f16021]) ).
fof(f16024,plain,
spl45_24,
inference(avatar_split_clause,[],[f10226,f16021]) ).
fof(f16043,definition,
( spl45_25
<=> m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK3))) ),
introduced(definition,[new_symbols(definition,[spl45_25])],[avatar_definition]) ).
fof(f16045,plain,
( m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl45_25 ),
inference(avatar_component_clause,[],[f16043]) ).
fof(f16046,plain,
spl45_25,
inference(avatar_split_clause,[],[f10224,f16043]) ).
fof(f16145,definition,
( spl45_26
<=> v4_rlvect_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl45_26])],[avatar_definition]) ).
fof(f16147,plain,
( v4_rlvect_1(sK2)
| ~ spl45_26 ),
inference(avatar_component_clause,[],[f16145]) ).
fof(f16148,plain,
spl45_26,
inference(avatar_split_clause,[],[f10213,f16145]) ).
fof(f16327,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) )
| ~ spl45_23 ),
inference(resolution,[],[f15208,f10203]) ).
fof(f16333,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) )
| ~ spl45_23 ),
inference(duplicate_literal_removal,[],[f16327]) ).
fof(f16337,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) )
| spl45_1
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16333,f10462]) ).
fof(f16340,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16337,f14069]) ).
fof(f16343,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_19
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16340,f14393]) ).
fof(f16346,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_12
| ~ spl45_19
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16343,f14074]) ).
fof(f16349,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) )
| spl45_1
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16346,f14084]) ).
fof(f16352,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) )
| spl45_1
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16349,f13940]) ).
fof(f16355,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) )
| spl45_1
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16352,f12648]) ).
fof(f16358,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16355,f10467]) ).
fof(f16361,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_20
| ~ spl45_23 ),
inference(forward_subsumption_resolution,[],[f16358,f14653]) ).
fof(f16364,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_20
| ~ spl45_23
| ~ spl45_26 ),
inference(forward_subsumption_resolution,[],[f16361,f16147]) ).
fof(f16367,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_23
| ~ spl45_26 ),
inference(forward_subsumption_resolution,[],[f16364,f14843]) ).
fof(f16370,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_22
| ~ spl45_23
| ~ spl45_26 ),
inference(forward_subsumption_resolution,[],[f16367,f15204]) ).
fof(f16373,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_22
| ~ spl45_23
| ~ spl45_26 ),
inference(forward_subsumption_resolution,[],[f16370,f14059]) ).
fof(f16376,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_18
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_22
| ~ spl45_23
| ~ spl45_26 ),
inference(forward_subsumption_resolution,[],[f16373,f14180]) ).
fof(f16379,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_18
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_22
| ~ spl45_23
| ~ spl45_26 ),
inference(forward_subsumption_resolution,[],[f16376,f14064]) ).
fof(f16382,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) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_18
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_22
| ~ spl45_23
| ~ spl45_26 ),
inference(forward_subsumption_resolution,[],[f16379,f14054]) ).
fof(f16385,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))) )
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_18
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_22
| ~ spl45_23
| ~ spl45_26 ),
inference(forward_subsumption_resolution,[],[f16382,f14049]) ).
fof(f16387,definition,
( spl45_27
<=> ! [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,[spl45_27])],[avatar_definition]) ).
fof(f16388,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))) )
| ~ spl45_27 ),
inference(avatar_component_clause,[],[f16387]) ).
fof(f16389,plain,
( spl45_27
| spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_18
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_22
| ~ spl45_23
| ~ spl45_26 ),
inference(avatar_split_clause,[],[f16385,f16145,f15207,f15202,f14841,f14651,f14391,f14178,f14082,f14072,f14067,f14062,f14057,f14052,f14047,f13938,f12646,f10465,f10460,f16387]) ).
fof(f16395,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))) )
| ~ spl45_25
| ~ spl45_27 ),
inference(resolution,[],[f16388,f16045]) ).
fof(f16407,plain,
( ! [X0] :
( v1_rmod_5(X0,sK2,sK3)
| ~ r1_tarski(X0,sK5)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3))) )
| ~ spl45_5
| ~ spl45_25
| ~ spl45_27 ),
inference(forward_subsumption_resolution,[],[f16395,f13935]) ).
fof(f16414,definition,
( spl45_28
<=> ! [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,[spl45_28])],[avatar_definition]) ).
fof(f16415,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ r1_tarski(X0,sK5)
| v1_rmod_5(X0,sK2,sK3) )
| ~ spl45_28 ),
inference(avatar_component_clause,[],[f16414]) ).
fof(f16416,plain,
( spl45_28
| ~ spl45_5
| ~ spl45_25
| ~ spl45_27 ),
inference(avatar_split_clause,[],[f16407,f16387,f16043,f13933,f16414]) ).
fof(f16421,plain,
( ~ r1_tarski(sK4,sK5)
| v1_rmod_5(sK4,sK2,sK3)
| ~ spl45_4
| ~ spl45_28 ),
inference(resolution,[],[f16415,f13833]) ).
fof(f16434,plain,
( v1_rmod_5(sK4,sK2,sK3)
| ~ spl45_4
| ~ spl45_24
| ~ spl45_28 ),
inference(forward_subsumption_resolution,[],[f16421,f16023]) ).
fof(f16437,plain,
( $false
| ~ spl45_4
| spl45_13
| ~ spl45_24
| ~ spl45_28 ),
inference(forward_subsumption_resolution,[],[f16434,f14079]) ).
fof(f16438,plain,
( ~ spl45_4
| spl45_13
| ~ spl45_24
| ~ spl45_28 ),
inference(avatar_contradiction_clause,[],[f16437]) ).
cnf(s1,plain,
~ spl45_1,
inference(sat_conversion,[],[f10463]) ).
cnf(s2,plain,
~ spl45_2,
inference(sat_conversion,[],[f10468]) ).
cnf(s3,plain,
spl45_3,
inference(sat_conversion,[],[f12649]) ).
cnf(s4,plain,
spl45_4,
inference(sat_conversion,[],[f13834]) ).
cnf(s5,plain,
spl45_5,
inference(sat_conversion,[],[f13936]) ).
cnf(s6,plain,
spl45_6,
inference(sat_conversion,[],[f13941]) ).
cnf(s7,plain,
spl45_7,
inference(sat_conversion,[],[f14050]) ).
cnf(s8,plain,
spl45_8,
inference(sat_conversion,[],[f14055]) ).
cnf(s9,plain,
spl45_9,
inference(sat_conversion,[],[f14060]) ).
cnf(s10,plain,
spl45_10,
inference(sat_conversion,[],[f14065]) ).
cnf(s11,plain,
spl45_11,
inference(sat_conversion,[],[f14070]) ).
cnf(s12,plain,
spl45_12,
inference(sat_conversion,[],[f14075]) ).
cnf(s13,plain,
~ spl45_13,
inference(sat_conversion,[],[f14080]) ).
cnf(s14,plain,
spl45_14,
inference(sat_conversion,[],[f14085]) ).
cnf(s15,plain,
( spl45_1
| spl45_2
| ~ spl45_3
| spl45_15 ),
inference(sat_conversion,[],[f14089]) ).
cnf(s16,plain,
( spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_15
| spl45_16 ),
inference(sat_conversion,[],[f14113]) ).
cnf(s18,plain,
spl45_18,
inference(sat_conversion,[],[f14181]) ).
cnf(s19,plain,
spl45_19,
inference(sat_conversion,[],[f14394]) ).
cnf(s20,plain,
spl45_20,
inference(sat_conversion,[],[f14654]) ).
cnf(s21,plain,
spl45_21,
inference(sat_conversion,[],[f14844]) ).
cnf(s22,plain,
spl45_22,
inference(sat_conversion,[],[f15205]) ).
cnf(s23,plain,
( spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_16
| spl45_23 ),
inference(sat_conversion,[],[f15209]) ).
cnf(s24,plain,
spl45_24,
inference(sat_conversion,[],[f16024]) ).
cnf(s25,plain,
spl45_25,
inference(sat_conversion,[],[f16046]) ).
cnf(s26,plain,
spl45_26,
inference(sat_conversion,[],[f16148]) ).
cnf(s27,plain,
( spl45_1
| spl45_2
| ~ spl45_3
| ~ spl45_6
| ~ spl45_7
| ~ spl45_8
| ~ spl45_9
| ~ spl45_10
| ~ spl45_11
| ~ spl45_12
| ~ spl45_14
| ~ spl45_18
| ~ spl45_19
| ~ spl45_20
| ~ spl45_21
| ~ spl45_22
| ~ spl45_23
| ~ spl45_26
| spl45_27 ),
inference(sat_conversion,[],[f16389]) ).
cnf(s28,plain,
( ~ spl45_5
| ~ spl45_25
| ~ spl45_27
| spl45_28 ),
inference(sat_conversion,[],[f16416]) ).
cnf(s29,plain,
( ~ spl45_4
| spl45_13
| ~ spl45_24
| ~ spl45_28 ),
inference(sat_conversion,[],[f16438]) ).
cnf(s30,plain,
~ spl45_28,
inference(rat,[],[s29,s13,s24,s4]) ).
cnf(s31,plain,
~ spl45_27,
inference(rat,[],[s28,s5,s25,s30]) ).
cnf(s32,plain,
~ spl45_23,
inference(rat,[],[s27,s31,s26,s2,s22,s21,s20,s19,s18,s14,s12,s11,s10,s9,s8,s7,s6,s3,s1]) ).
cnf(s33,plain,
~ spl45_16,
inference(rat,[],[s23,s32,s2,s14,s12,s11,s10,s9,s8,s7,s6,s3,s1]) ).
cnf(s34,plain,
~ spl45_15,
inference(rat,[],[s16,s33,s2,s14,s12,s11,s10,s9,s8,s7,s6,s3,s1]) ).
cnf(s35,plain,
$false,
inference(rat,[],[s15,s2,s3,s34,s1]) ).
fof(f16444,plain,
$false,
inference(avatar_sat_refutation,[],[s35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG214+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n004.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 19:44:39 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running first-order theorem proving
% 0.07/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
% 11.56/2.78 % (683632)Detected formulas, will run a generic FOF schedule.
% 11.56/2.78 % (683641)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3259751836:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 11.56/2.78 % (683640)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1887956057:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 11.56/2.78 % (683637)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=2212992159:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 11.56/2.78 % (683639)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=293829829:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 11.56/2.78 % (683638)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=3175977401:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 11.56/2.78 % (683642)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3664663119:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 11.56/2.78 % (683643)dis-21_1_sil=8000:lcm=predicate:random_seed=1899736735:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 11.56/2.78 % (683641)Instruction limit reached!
% 11.56/2.78 % (683641)------------------------------
% 11.56/2.78 % (683641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683641)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683641)Termination reason: Instruction limit
% 11.56/2.78 % (683641)Termination phase: Property scanning
% 11.56/2.78 % (683641)Time elapsed: 0.054 s
% 11.56/2.78 % (683641)Peak memory usage: 100 MB
% 11.56/2.78 % (683641)Instructions burned: 124 (million)
% 11.56/2.78 % (683642)Instruction limit reached!
% 11.56/2.78 % (683642)------------------------------
% 11.56/2.78 % (683642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683642)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683642)Termination reason: Instruction limit
% 11.56/2.78 % (683642)Termination phase: SInE selection
% 11.56/2.78 % (683642)Time elapsed: 0.065 s
% 11.56/2.78 % (683642)Peak memory usage: 97 MB
% 11.56/2.78 % (683642)Instructions burned: 139 (million)
% 11.56/2.78 % (683640)Instruction limit reached!
% 11.56/2.78 % (683640)------------------------------
% 11.56/2.78 % (683640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683640)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683640)Termination reason: Instruction limit
% 11.56/2.78 % (683640)Termination phase: Saturation
% 11.56/2.78 % (683640)Time elapsed: 0.078 s
% 11.56/2.78 % (683640)Peak memory usage: 101 MB
% 11.56/2.78 % (683640)Instructions burned: 110 (million)
% 11.56/2.78 % (683651)lrs+10_1_sil=8000:sp=occurrence:random_seed=1105522318:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 11.56/2.78 % (683643)Instruction limit reached!
% 11.56/2.78 % (683643)------------------------------
% 11.56/2.78 % (683643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683643)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683643)Termination reason: Instruction limit
% 11.56/2.78 % (683643)Termination phase: Unused predicate definition removal
% 11.56/2.78 % (683643)Time elapsed: 0.104 s
% 11.56/2.78 % (683643)Peak memory usage: 99 MB
% 11.56/2.78 % (683643)Instructions burned: 129 (million)
% 11.56/2.78 % (683652)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1367430768:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 11.56/2.78 % (683653)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1061447300:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 11.56/2.78 % (683651)Instruction limit reached!
% 11.56/2.78 % (683651)------------------------------
% 11.56/2.78 % (683651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683651)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683651)Termination reason: Instruction limit
% 11.56/2.78 % (683651)Termination phase: Saturation
% 11.56/2.78 % (683651)Time elapsed: 0.105 s
% 11.56/2.78 % (683651)Peak memory usage: 103 MB
% 11.56/2.78 % (683651)Instructions burned: 287 (million)
% 11.56/2.78 % (683655)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=2301354770:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 11.56/2.78 % (683652)Instruction limit reached!
% 11.56/2.78 % (683652)------------------------------
% 11.56/2.78 % (683652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683652)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683652)Termination reason: Instruction limit
% 11.56/2.78 % (683652)Termination phase: SInE selection
% 11.56/2.78 % (683652)Time elapsed: 0.080 s
% 11.56/2.78 % (683652)Peak memory usage: 97 MB
% 11.56/2.78 % (683652)Instructions burned: 158 (million)
% 11.56/2.78 % (683658)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3426786681:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 11.56/2.78 % (683655)Instruction limit reached!
% 11.56/2.78 % (683655)------------------------------
% 11.56/2.78 % (683655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683655)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683655)Termination reason: Instruction limit
% 11.56/2.78 % (683655)Termination phase: Preprocessing 1
% 11.56/2.78 % (683655)Time elapsed: 0.145 s
% 11.56/2.78 % (683655)Peak memory usage: 97 MB
% 11.56/2.78 % (683655)Instructions burned: 249 (million)
% 11.56/2.78 % (683660)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2737940250:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 11.56/2.78 % (683658)Instruction limit reached!
% 11.56/2.78 % (683658)------------------------------
% 11.56/2.78 % (683658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683658)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683658)Termination reason: Instruction limit
% 11.56/2.78 % (683658)Termination phase: Saturation
% 11.56/2.78 % (683658)Time elapsed: 0.099 s
% 11.56/2.78 % (683658)Peak memory usage: 104 MB
% 11.56/2.78 % (683658)Instructions burned: 295 (million)
% 11.56/2.78 % (683653)Instruction limit reached!
% 11.56/2.78 % (683653)------------------------------
% 11.56/2.78 % (683653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683653)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683653)Termination reason: Instruction limit
% 11.56/2.78 % (683653)Termination phase: Saturation
% 11.56/2.78 % (683653)Time elapsed: 0.236 s
% 11.56/2.78 % (683653)Peak memory usage: 103 MB
% 11.56/2.78 % (683653)Instructions burned: 326 (million)
% 11.56/2.78 % (683664)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3429914608:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 11.56/2.78 % (683663)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=844017299:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 11.56/2.78 % (683664)Instruction limit reached!
% 11.56/2.78 % (683664)------------------------------
% 11.56/2.78 % (683664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683664)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683664)Termination reason: Instruction limit
% 11.56/2.78 % (683664)Termination phase: Naming
% 11.56/2.78 % (683664)Time elapsed: 0.060 s
% 11.56/2.78 % (683664)Peak memory usage: 106 MB
% 11.56/2.78 % (683664)Instructions burned: 128 (million)
% 11.56/2.78 % (683665)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3631618571:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 11.56/2.78 % (683663)Instruction limit reached!
% 11.56/2.78 % (683663)------------------------------
% 11.56/2.78 % (683663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683663)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683663)Termination reason: Instruction limit
% 11.56/2.78 % (683663)Termination phase: Clausification
% 11.56/2.78 % (683663)Time elapsed: 0.091 s
% 11.56/2.78 % (683663)Peak memory usage: 100 MB
% 11.56/2.78 % (683663)Instructions burned: 113 (million)
% 11.56/2.78 % (683665)Instruction limit reached!
% 11.56/2.78 % (683665)------------------------------
% 11.56/2.78 % (683665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683665)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683665)Termination reason: Instruction limit
% 11.56/2.78 % (683665)Termination phase: Property scanning
% 11.56/2.78 % (683665)Time elapsed: 0.050 s
% 11.56/2.78 % (683665)Peak memory usage: 96 MB
% 11.56/2.78 % (683665)Instructions burned: 116 (million)
% 11.56/2.78 % (683668)lrs+10_1_sil=8000:sp=occurrence:random_seed=2142944283:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 11.56/2.78 % (683670)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3330599599:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 11.56/2.78 % (683671)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=505910396:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 11.56/2.78 % (683668)Instruction limit reached!
% 11.56/2.78 % (683668)------------------------------
% 11.56/2.78 % (683668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683668)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683668)Termination reason: Instruction limit
% 11.56/2.78 % (683668)Termination phase: Saturation
% 11.56/2.78 % (683668)Time elapsed: 0.294 s
% 11.56/2.78 % (683668)Peak memory usage: 116 MB
% 11.56/2.78 % (683668)Instructions burned: 907 (million)
% 11.56/2.78 % (683670)Instruction limit reached!
% 11.56/2.78 % (683670)------------------------------
% 11.56/2.78 % (683670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683670)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683670)Termination reason: Instruction limit
% 11.56/2.78 % (683670)Termination phase: Saturation
% 11.56/2.78 % (683670)Time elapsed: 0.271 s
% 11.56/2.78 % (683670)Peak memory usage: 103 MB
% 11.56/2.78 % (683670)Instructions burned: 439 (million)
% 11.56/2.78 % (683675)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1858219650:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 11.56/2.78 % (683675)Instruction limit reached!
% 11.56/2.78 % (683675)------------------------------
% 11.56/2.78 % (683675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683675)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683675)Termination reason: Instruction limit
% 11.56/2.78 % (683675)Termination phase: Saturation
% 11.56/2.78 % (683675)Time elapsed: 0.055 s
% 11.56/2.78 % (683675)Peak memory usage: 103 MB
% 11.56/2.78 % (683675)Instructions burned: 136 (million)
% 11.56/2.78 % (683676)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1360071730:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 11.56/2.78 % (683678)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3433757156:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 11.56/2.78 % (683639)First to succeed.
% 11.56/2.78 % (683639)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-683632"
% 11.56/2.78 % (683676)Instruction limit reached!
% 11.56/2.78 % (683676)------------------------------
% 11.56/2.78 % (683676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.78 % (683676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.78 % (683676)CaDiCaL version: 2.1.3
% 11.56/2.78 % (683676)Termination reason: Instruction limit
% 11.56/2.78 % (683676)Termination phase: Property scanning
% 11.56/2.78 % (683676)Time elapsed: 0.352 s
% 11.56/2.78 % (683676)Peak memory usage: 113 MB
% 11.56/2.78 % (683676)Instructions burned: 597 (million)
% 11.56/2.78 % (683639)Refutation found. Thanks to Tanya!
% 11.56/2.78 % SZS status Theorem for theBenchmark
% 11.56/2.78 % SZS output start Proof for theBenchmark
% See solution above
% 12.99/3.01 % (683639)------------------------------
% 12.99/3.01 % (683639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.99/3.01 % (683639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.99/3.01 % (683639)CaDiCaL version: 2.1.3
% 12.99/3.01 % (683639)Termination reason: Refutation
% 12.99/3.01 % (683639)Time elapsed: 1.285 s
% 12.99/3.01 % (683639)Peak memory usage: 150 MB
% 12.99/3.01 % (683639)Instructions burned: 2186 (million)
% 12.99/3.01 % (683639)------------------------------
% 12.99/3.01 % (683639)------------------------------
% 12.99/3.01 % (683632)Success in time 2.161 s
% 12.99/3.01 % Vampire exiting
%------------------------------------------------------------------------------