%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG218+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:19:23 AM UTC 2026
% Result : Theorem 111.02s 17.47s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 71
% Syntax : Number of formulae : 358 ( 111 unt; 49 def)
% Number of atoms : 1758 ( 173 equ)
% Maximal formula atoms : 24 ( 4 avg)
% Number of connectives : 2406 (1006 ~;1082 |; 224 &)
% ( 58 <=>; 35 =>; 0 <=; 1 <~>)
% Maximal formula depth : 28 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 72 ( 70 usr; 44 prp; 0-4 aty)
% Number of functors : 24 ( 24 usr; 11 con; 0-3 aty)
% Number of variables : 243 ( 0 sgn 230 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
<=> r2_hidden(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(f4,axiom,
! [X0,X1] :
( X1 = k1_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tarski) ).
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f72,axiom,
! [X0] :
( r1_tarski(X0,k1_xboole_0)
=> X0 = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_xboole_1) ).
fof(f438,axiom,
! [X0,X1] :
( k2_zfmisc_1(X0,X1) = k1_xboole_0
<=> ( X0 = k1_xboole_0
| X1 = k1_xboole_0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t113_zfmisc_1) ).
fof(f455,axiom,
! [X0,X1] :
( X0 != k1_xboole_0
=> ( k2_zfmisc_1(k1_tarski(X1),X0) != k1_xboole_0
& k2_zfmisc_1(X0,k1_tarski(X1)) != k1_xboole_0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t130_zfmisc_1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f1638,axiom,
! [X0] :
~ ( X0 != k1_xboole_0
& ! [X1] :
~ ( r2_hidden(X1,X0)
& ! [X2] :
( r2_hidden(X2,X1)
=> r1_xboole_0(X2,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_mcart_1) ).
fof(f3551,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f6430,axiom,
! [X0] :
( l2_struct_0(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_struct_0) ).
fof(f7207,axiom,
! [X0] :
( l1_rlvect_1(X0)
=> l2_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_rlvect_1) ).
fof(f7537,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_vectsp_1(X0) )
=> ( v10_vectsp_1(X0)
<=> k1_rlvect_1(X0) = k2_group_1(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d21_vectsp_1) ).
fof(f7635,axiom,
! [X0] :
( l2_vectsp_1(X0)
=> ( l1_vectsp_1(X0)
& l2_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_vectsp_1) ).
fof(f7637,axiom,
! [X0] :
( l3_vectsp_1(X0)
=> ( l1_rlvect_1(X0)
& l2_vectsp_1(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_vectsp_1) ).
fof(f8148,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k7_rlvect_2(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k7_rlvect_2) ).
fof(f8549,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( l1_vectsp_2(X1,X0)
=> l1_rlvect_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_vectsp_2) ).
fof(f9718,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) )
=> m1_rmod_2(X1,X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_rmod_2) ).
fof(f9734,axiom,
! [X0,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) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ( r1_rlvect_1(k1_rmod_2(X1,X2),X0)
<=> X0 = k1_rlvect_1(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_rmod_2) ).
fof(f9775,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_rmod_2(X2,X0,X1)
=> m2_rmod_2(u1_struct_0(X2),X0,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t86_rmod_2) ).
fof(f9778,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_rmod_2(X2,X0,X1)
=> ! [X3] :
( m2_rmod_2(X3,X0,X1,X2)
=> ( r2_hidden(k1_rlvect_1(X1),X3)
<=> X3 = u1_struct_0(X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t89_rmod_2) ).
fof(f10001,axiom,
! [X0,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)
& v7_group_1(X1)
& v6_vectsp_1(X1)
& v7_vectsp_1(X1)
& v8_vectsp_1(X1)
& ~ v10_vectsp_1(X1)
& v2_vectsp_2(X1)
& l3_vectsp_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X1)
& l1_vectsp_2(X2,X1) )
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))
=> ( r2_hidden(X0,X3)
=> r1_rlvect_1(k1_rmod_5(X1,X2,X3),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_rmod_5) ).
fof(f10003,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)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(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)))
=> ~ ( k1_rmod_5(X0,X1,X2) = k1_rmod_2(X0,X1)
& X2 != k1_xboole_0
& X2 != k7_rlvect_2(X1,k1_rlvect_1(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_rmod_5) ).
fof(f10004,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)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(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)))
=> ~ ( k1_rmod_5(X0,X1,X2) = k1_rmod_2(X0,X1)
& X2 != k1_xboole_0
& X2 != k7_rlvect_2(X1,k1_rlvect_1(X1)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f10003]) ).
fof(f10102,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_rmod_5(X0,X1,X2) = k1_rmod_2(X0,X1)
& X2 != k1_xboole_0
& X2 != k7_rlvect_2(X1,k1_rlvect_1(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)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f10004]) ).
fof(f10103,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_rmod_5(X0,X1,X2) = k1_rmod_2(X0,X1)
& X2 != k1_xboole_0
& X2 != k7_rlvect_2(X1,k1_rlvect_1(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)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) ),
inference(flattening,[],[f10102]) ).
fof(f10141,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ r1_tarski(X0,k1_xboole_0) ),
inference(ennf_transformation,[],[f72]) ).
fof(f10210,plain,
! [X0,X1] :
( k7_rlvect_2(X0,X1) = k1_tarski(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f8148]) ).
fof(f10211,plain,
! [X0,X1] :
( k7_rlvect_2(X0,X1) = k1_tarski(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f10210]) ).
fof(f10244,plain,
! [X0,X1] :
( ! [X2] :
( ( r1_rlvect_1(k1_rmod_2(X1,X2),X0)
<=> X0 = k1_rlvect_1(X2) )
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,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) ),
inference(ennf_transformation,[],[f9734]) ).
fof(f10245,plain,
! [X0,X1] :
( ! [X2] :
( ( r1_rlvect_1(k1_rmod_2(X1,X2),X0)
<=> X0 = k1_rlvect_1(X2) )
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,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) ),
inference(flattening,[],[f10244]) ).
fof(f10250,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r1_rlvect_1(k1_rmod_5(X1,X2,X3),X0)
| ~ r2_hidden(X0,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2))) )
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,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)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) ),
inference(ennf_transformation,[],[f10001]) ).
fof(f10251,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r1_rlvect_1(k1_rmod_5(X1,X2,X3),X0)
| ~ r2_hidden(X0,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2))) )
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,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)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) ),
inference(flattening,[],[f10250]) ).
fof(f10325,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f10332,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f10336,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f10574,plain,
! [X0] :
( ( l1_rlvect_1(X0)
& l2_vectsp_1(X0) )
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f7637]) ).
fof(f10575,plain,
! [X0] :
( ( l1_vectsp_1(X0)
& l2_struct_0(X0) )
| ~ l2_vectsp_1(X0) ),
inference(ennf_transformation,[],[f7635]) ).
fof(f10576,plain,
! [X0] :
( ( v10_vectsp_1(X0)
<=> k1_rlvect_1(X0) = k2_group_1(X0) )
| v3_struct_0(X0)
| ~ l2_vectsp_1(X0) ),
inference(ennf_transformation,[],[f7537]) ).
fof(f10577,plain,
! [X0] :
( ( v10_vectsp_1(X0)
<=> k1_rlvect_1(X0) = k2_group_1(X0) )
| v3_struct_0(X0)
| ~ l2_vectsp_1(X0) ),
inference(flattening,[],[f10576]) ).
fof(f10649,plain,
! [X0] :
( ! [X1] :
( m1_rmod_2(X1,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) )
| 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,[],[f9718]) ).
fof(f10650,plain,
! [X0] :
( ! [X1] :
( m1_rmod_2(X1,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) )
| 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,[],[f10649]) ).
fof(f10723,plain,
! [X0,X1] :
( ( k2_zfmisc_1(k1_tarski(X1),X0) != k1_xboole_0
& k2_zfmisc_1(X0,k1_tarski(X1)) != k1_xboole_0 )
| k1_xboole_0 = X0 ),
inference(ennf_transformation,[],[f455]) ).
fof(f10733,plain,
! [X0] :
( ! [X1] :
( l1_rlvect_1(X1)
| ~ l1_vectsp_2(X1,X0) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f8549]) ).
fof(f10999,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(k1_rlvect_1(X1),X3)
<=> X3 = u1_struct_0(X2) )
| ~ m2_rmod_2(X3,X0,X1,X2) )
| ~ m1_rmod_2(X2,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) )
| 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,[],[f9778]) ).
fof(f11000,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(k1_rlvect_1(X1),X3)
<=> X3 = u1_struct_0(X2) )
| ~ m2_rmod_2(X3,X0,X1,X2) )
| ~ m1_rmod_2(X2,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) )
| 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,[],[f10999]) ).
fof(f11001,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m2_rmod_2(u1_struct_0(X2),X0,X1,X2)
| ~ m1_rmod_2(X2,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) )
| 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,[],[f9775]) ).
fof(f11002,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m2_rmod_2(u1_struct_0(X2),X0,X1,X2)
| ~ m1_rmod_2(X2,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) )
| 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,[],[f11001]) ).
fof(f11406,plain,
! [X0] :
( l2_struct_0(X0)
| ~ l1_rlvect_1(X0) ),
inference(ennf_transformation,[],[f7207]) ).
fof(f11409,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_struct_0(X0) ),
inference(ennf_transformation,[],[f6430]) ).
fof(f11511,plain,
! [X0] :
( k1_xboole_0 = X0
| ? [X1] :
( r2_hidden(X1,X0)
& ! [X2] :
( r1_xboole_0(X2,X0)
| ~ r2_hidden(X2,X1) ) ) ),
inference(ennf_transformation,[],[f1638]) ).
fof(f12169,plain,
( k1_rmod_2(sK27,sK28) = k1_rmod_5(sK27,sK28,sK29)
& k1_xboole_0 != sK29
& sK29 != k7_rlvect_2(sK28,k1_rlvect_1(sK28))
& m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK28)))
& ~ v3_struct_0(sK28)
& v3_rlvect_1(sK28)
& v4_rlvect_1(sK28)
& v5_rlvect_1(sK28)
& v6_rlvect_1(sK28)
& v5_vectsp_2(sK28,sK27)
& l1_vectsp_2(sK28,sK27)
& ~ v3_struct_0(sK27)
& v3_rlvect_1(sK27)
& v4_rlvect_1(sK27)
& v5_rlvect_1(sK27)
& v6_rlvect_1(sK27)
& v4_group_1(sK27)
& v7_group_1(sK27)
& v6_vectsp_1(sK27)
& v7_vectsp_1(sK27)
& v8_vectsp_1(sK27)
& ~ v10_vectsp_1(sK27)
& v2_vectsp_2(sK27)
& l3_vectsp_1(sK27) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29]),skolemize(X0,sK27),skolemize(X1,sK28),skolemize(X2,sK29)],[f10103]) ).
fof(f12173,plain,
! [X0,X1] :
( ( k2_zfmisc_1(X0,X1) = k1_xboole_0
| ( k1_xboole_0 != X0
& k1_xboole_0 != X1 ) )
& ( X0 = k1_xboole_0
| X1 = k1_xboole_0
| k1_xboole_0 != k2_zfmisc_1(X0,X1) ) ),
inference(nnf_transformation,[],[f438]) ).
fof(f12174,plain,
! [X0,X1] :
( ( k2_zfmisc_1(X0,X1) = k1_xboole_0
| ( k1_xboole_0 != X0
& k1_xboole_0 != X1 ) )
& ( X0 = k1_xboole_0
| X1 = k1_xboole_0
| k1_xboole_0 != k2_zfmisc_1(X0,X1) ) ),
inference(flattening,[],[f12173]) ).
fof(f12209,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r1_rlvect_1(k1_rmod_2(X1,X2),X0)
| k1_rlvect_1(X2) != X0 )
& ( X0 = k1_rlvect_1(X2)
| ~ r1_rlvect_1(k1_rmod_2(X1,X2),X0) ) )
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,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) ),
inference(nnf_transformation,[],[f10245]) ).
fof(f12231,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f10325]) ).
fof(f12232,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f12231]) ).
fof(f12233,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK70(X0,X1),X1)
& r2_hidden(sK70(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70]),skolemize(X2,sK70(X0,X1))],[f12232]) ).
fof(f12236,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( ( ~ r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
& ( r2_hidden(X2,X1)
| r2_hidden(X2,X0) ) ) ),
inference(nnf_transformation,[],[f10336]) ).
fof(f12237,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK72(X0,X1),X1)
| ~ r2_hidden(sK72(X0,X1),X0) )
& ( r2_hidden(sK72(X0,X1),X1)
| r2_hidden(sK72(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72]),skolemize(X2,sK72(X0,X1))],[f12236]) ).
fof(f12308,plain,
! [X0] :
( ( ( v10_vectsp_1(X0)
| k1_rlvect_1(X0) != k2_group_1(X0) )
& ( k1_rlvect_1(X0) = k2_group_1(X0)
| ~ v10_vectsp_1(X0) ) )
| v3_struct_0(X0)
| ~ l2_vectsp_1(X0) ),
inference(nnf_transformation,[],[f10577]) ).
fof(f12366,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ? [X2] :
( ( X0 != X2
| ~ r2_hidden(X2,X1) )
& ( X2 = X0
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| X0 != X2 )
& ( X2 = X0
| ~ r2_hidden(X2,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f12367,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ? [X2] :
( ( X0 != X2
| ~ r2_hidden(X2,X1) )
& ( X2 = X0
| r2_hidden(X2,X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ r2_hidden(X3,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(rectify,[],[f12366]) ).
fof(f12368,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ( ( sK162(X0,X1) != X0
| ~ r2_hidden(sK162(X0,X1),X1) )
& ( sK162(X0,X1) = X0
| r2_hidden(sK162(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ r2_hidden(X3,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK162]),skolemize(X2,sK162(X0,X1))],[f12367]) ).
fof(f12433,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(k1_rlvect_1(X1),X3)
| u1_struct_0(X2) != X3 )
& ( X3 = u1_struct_0(X2)
| ~ r2_hidden(k1_rlvect_1(X1),X3) ) )
| ~ m2_rmod_2(X3,X0,X1,X2) )
| ~ m1_rmod_2(X2,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) )
| 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,[],[f11000]) ).
fof(f12588,plain,
! [X0] :
( k1_xboole_0 = X0
| ( r2_hidden(sK285(X0),X0)
& ! [X2] :
( r1_xboole_0(X2,X0)
| ~ r2_hidden(X2,sK285(X0)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK285]),skolemize(X1,sK285(X0))],[f11511]) ).
fof(f12825,plain,
l3_vectsp_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12826,plain,
v2_vectsp_2(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12827,plain,
~ v10_vectsp_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12828,plain,
v8_vectsp_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12829,plain,
v7_vectsp_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12830,plain,
v6_vectsp_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12831,plain,
v7_group_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12832,plain,
v4_group_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12833,plain,
v6_rlvect_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12834,plain,
v5_rlvect_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12835,plain,
v4_rlvect_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12836,plain,
v3_rlvect_1(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12837,plain,
~ v3_struct_0(sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12838,plain,
l1_vectsp_2(sK28,sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12839,plain,
v5_vectsp_2(sK28,sK27),
inference(cnf_transformation,[],[f12169]) ).
fof(f12840,plain,
v6_rlvect_1(sK28),
inference(cnf_transformation,[],[f12169]) ).
fof(f12841,plain,
v5_rlvect_1(sK28),
inference(cnf_transformation,[],[f12169]) ).
fof(f12842,plain,
v4_rlvect_1(sK28),
inference(cnf_transformation,[],[f12169]) ).
fof(f12843,plain,
v3_rlvect_1(sK28),
inference(cnf_transformation,[],[f12169]) ).
fof(f12844,plain,
~ v3_struct_0(sK28),
inference(cnf_transformation,[],[f12169]) ).
fof(f12845,plain,
m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK28))),
inference(cnf_transformation,[],[f12169]) ).
fof(f12846,plain,
sK29 != k7_rlvect_2(sK28,k1_rlvect_1(sK28)),
inference(cnf_transformation,[],[f12169]) ).
fof(f12847,plain,
k1_xboole_0 != sK29,
inference(cnf_transformation,[],[f12169]) ).
fof(f12848,plain,
k1_rmod_2(sK27,sK28) = k1_rmod_5(sK27,sK28,sK29),
inference(cnf_transformation,[],[f12169]) ).
fof(f12902,plain,
! [X0,X1] :
( k1_xboole_0 = k2_zfmisc_1(X0,X1)
| k1_xboole_0 != X1 ),
inference(cnf_transformation,[],[f12174]) ).
fof(f12904,plain,
! [X0] :
( k1_xboole_0 = X0
| ~ r1_tarski(X0,k1_xboole_0) ),
inference(cnf_transformation,[],[f10141]) ).
fof(f13025,plain,
! [X0,X1] :
( k1_tarski(X1) = k7_rlvect_2(X0,X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f10211]) ).
fof(f13048,plain,
! [X2,X0,X1] :
( ~ r1_rlvect_1(k1_rmod_2(X1,X2),X0)
| k1_rlvect_1(X2) = X0
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,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) ),
inference(cnf_transformation,[],[f12209]) ).
fof(f13053,plain,
! [X2,X3,X0,X1] :
( r1_rlvect_1(k1_rmod_5(X1,X2,X3),X0)
| ~ r2_hidden(X0,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2)))
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,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)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) ),
inference(cnf_transformation,[],[f10251]) ).
fof(f13151,plain,
! [X0,X1] :
( r2_hidden(sK70(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f12233]) ).
fof(f13158,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f10332]) ).
fof(f13166,plain,
! [X0,X1] :
( r2_hidden(sK72(X0,X1),X1)
| X0 = X1
| r2_hidden(sK72(X0,X1),X0) ),
inference(cnf_transformation,[],[f12237]) ).
fof(f13167,plain,
! [X0,X1] :
( ~ r2_hidden(sK72(X0,X1),X1)
| X0 = X1
| ~ r2_hidden(sK72(X0,X1),X0) ),
inference(cnf_transformation,[],[f12237]) ).
fof(f13440,plain,
! [X0] :
( l2_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f10574]) ).
fof(f13443,plain,
! [X0] :
( ~ l2_vectsp_1(X0)
| l2_struct_0(X0) ),
inference(cnf_transformation,[],[f10575]) ).
fof(f13446,plain,
! [X0] :
( k1_rlvect_1(X0) != k2_group_1(X0)
| v10_vectsp_1(X0)
| v3_struct_0(X0)
| ~ l2_vectsp_1(X0) ),
inference(cnf_transformation,[],[f12308]) ).
fof(f13654,plain,
! [X0,X1] :
( m1_rmod_2(X1,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)
| 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,[],[f10650]) ).
fof(f13723,plain,
! [X0,X1] :
( k1_xboole_0 != k2_zfmisc_1(X0,k1_tarski(X1))
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f10723]) ).
fof(f13759,plain,
! [X3,X0,X1] :
( k1_tarski(X0) != X1
| ~ r2_hidden(X3,X1)
| X0 = X3 ),
inference(cnf_transformation,[],[f12368]) ).
fof(f13764,plain,
! [X0,X1] :
( l1_rlvect_1(X1)
| ~ l1_vectsp_2(X1,X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f10733]) ).
fof(f14035,plain,
! [X2,X3,X0,X1] :
( u1_struct_0(X2) != X3
| r2_hidden(k1_rlvect_1(X1),X3)
| ~ m2_rmod_2(X3,X0,X1,X2)
| ~ m1_rmod_2(X2,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)
| 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,[],[f12433]) ).
fof(f14036,plain,
! [X2,X0,X1] :
( m2_rmod_2(u1_struct_0(X2),X0,X1,X2)
| ~ m1_rmod_2(X2,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)
| 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,[],[f11002]) ).
fof(f14457,plain,
! [X0] :
( l2_struct_0(X0)
| ~ l1_rlvect_1(X0) ),
inference(cnf_transformation,[],[f11406]) ).
fof(f14461,plain,
! [X0] :
( ~ l2_struct_0(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f11409]) ).
fof(f14651,plain,
! [X0] :
( k1_xboole_0 = X0
| r2_hidden(sK285(X0),X0) ),
inference(cnf_transformation,[],[f12588]) ).
fof(f15073,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f3551]) ).
fof(f15418,plain,
np__0 != sK29,
inference(definition_unfolding,[],[f12847,f15073]) ).
fof(f15468,plain,
! [X0,X1] :
( np__0 != X1
| k2_zfmisc_1(X0,X1) = np__0 ),
inference(definition_unfolding,[],[f12902,f15073,f15073]) ).
fof(f15470,plain,
! [X0] :
( ~ r1_tarski(X0,np__0)
| np__0 = X0 ),
inference(definition_unfolding,[],[f12904,f15073,f15073]) ).
fof(f15514,plain,
! [X0,X1] :
( k2_zfmisc_1(X0,k1_tarski(X1)) != np__0
| np__0 = X0 ),
inference(definition_unfolding,[],[f13723,f15073,f15073]) ).
fof(f15640,plain,
! [X0] :
( r2_hidden(sK285(X0),X0)
| np__0 = X0 ),
inference(definition_unfolding,[],[f14651,f15073]) ).
fof(f15765,definition,
sF437 = k1_rmod_2(sK27,sK28),
introduced(definition,[new_symbols(definition,[sF437])],[function_definition]) ).
fof(f15766,plain,
k1_rmod_2(sK27,sK28) = sF437,
inference(reorient_equations,[],[f15765]) ).
fof(f15767,definition,
sF438 = k1_rmod_5(sK27,sK28,sK29),
introduced(definition,[new_symbols(definition,[sF438])],[function_definition]) ).
fof(f15768,plain,
k1_rmod_5(sK27,sK28,sK29) = sF438,
inference(reorient_equations,[],[f15767]) ).
fof(f15769,plain,
sF437 = sF438,
inference(definition_folding,[],[f12848,f15768,f15766]) ).
fof(f15770,definition,
sF439 = k1_rlvect_1(sK28),
introduced(definition,[new_symbols(definition,[sF439])],[function_definition]) ).
fof(f15771,plain,
k1_rlvect_1(sK28) = sF439,
inference(reorient_equations,[],[f15770]) ).
fof(f15772,definition,
sF440 = k7_rlvect_2(sK28,sF439),
introduced(definition,[new_symbols(definition,[sF440])],[function_definition]) ).
fof(f15773,plain,
k7_rlvect_2(sK28,sF439) = sF440,
inference(reorient_equations,[],[f15772]) ).
fof(f15774,plain,
sK29 != sF440,
inference(definition_folding,[],[f12846,f15773,f15771]) ).
fof(f15775,definition,
sF441 = u1_struct_0(sK28),
introduced(definition,[new_symbols(definition,[sF441])],[function_definition]) ).
fof(f15776,plain,
u1_struct_0(sK28) = sF441,
inference(reorient_equations,[],[f15775]) ).
fof(f15777,definition,
sF442 = k1_zfmisc_1(sF441),
introduced(definition,[new_symbols(definition,[sF442])],[function_definition]) ).
fof(f15778,plain,
k1_zfmisc_1(sF441) = sF442,
inference(reorient_equations,[],[f15777]) ).
fof(f15779,plain,
m1_subset_1(sK29,sF442),
inference(definition_folding,[],[f12845,f15778,f15776]) ).
fof(f15796,definition,
( spl443_1
<=> l2_struct_0(sK28) ),
introduced(definition,[new_symbols(definition,[spl443_1])],[avatar_definition]) ).
fof(f15797,plain,
( l2_struct_0(sK28)
| ~ spl443_1 ),
inference(avatar_component_clause,[],[f15796]) ).
fof(f15798,plain,
( ~ l2_struct_0(sK28)
| spl443_1 ),
inference(avatar_component_clause,[],[f15796]) ).
fof(f15800,definition,
( spl443_2
<=> m1_subset_1(sF439,sF441) ),
introduced(definition,[new_symbols(definition,[spl443_2])],[avatar_definition]) ).
fof(f15801,plain,
( ~ m1_subset_1(sF439,sF441)
| spl443_2 ),
inference(avatar_component_clause,[],[f15800]) ).
fof(f15805,plain,
! [X0] :
( ~ r1_rlvect_1(sF437,X0)
| k1_rlvect_1(sK28) = X0
| v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| ~ l3_vectsp_1(sK27) ),
inference(superposition,[],[f13048,f15766]) ).
fof(f15806,plain,
! [X0] :
( sF439 = X0
| ~ r1_rlvect_1(sF437,X0)
| v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| ~ l3_vectsp_1(sK27) ),
inference(forward_demodulation,[],[f15805,f15771]) ).
fof(f15808,definition,
( spl443_3
<=> l3_vectsp_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_3])],[avatar_definition]) ).
fof(f15812,definition,
( spl443_4
<=> v8_vectsp_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_4])],[avatar_definition]) ).
fof(f15813,plain,
( v8_vectsp_1(sK27)
| ~ spl443_4 ),
inference(avatar_component_clause,[],[f15812]) ).
fof(f15816,definition,
( spl443_5
<=> v7_vectsp_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_5])],[avatar_definition]) ).
fof(f15820,definition,
( spl443_6
<=> v6_vectsp_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_6])],[avatar_definition]) ).
fof(f15824,definition,
( spl443_7
<=> v4_group_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_7])],[avatar_definition]) ).
fof(f15828,definition,
( spl443_8
<=> v6_rlvect_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_8])],[avatar_definition]) ).
fof(f15832,definition,
( spl443_9
<=> v5_rlvect_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_9])],[avatar_definition]) ).
fof(f15836,definition,
( spl443_10
<=> v4_rlvect_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_10])],[avatar_definition]) ).
fof(f15840,definition,
( spl443_11
<=> v3_rlvect_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_11])],[avatar_definition]) ).
fof(f15844,definition,
( spl443_12
<=> v3_struct_0(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_12])],[avatar_definition]) ).
fof(f15848,definition,
( spl443_13
<=> l1_vectsp_2(sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl443_13])],[avatar_definition]) ).
fof(f15852,definition,
( spl443_14
<=> v5_vectsp_2(sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl443_14])],[avatar_definition]) ).
fof(f15853,plain,
( v5_vectsp_2(sK28,sK27)
| ~ spl443_14 ),
inference(avatar_component_clause,[],[f15852]) ).
fof(f15856,definition,
( spl443_15
<=> v6_rlvect_1(sK28) ),
introduced(definition,[new_symbols(definition,[spl443_15])],[avatar_definition]) ).
fof(f15860,definition,
( spl443_16
<=> v5_rlvect_1(sK28) ),
introduced(definition,[new_symbols(definition,[spl443_16])],[avatar_definition]) ).
fof(f15864,definition,
( spl443_17
<=> v4_rlvect_1(sK28) ),
introduced(definition,[new_symbols(definition,[spl443_17])],[avatar_definition]) ).
fof(f15868,definition,
( spl443_18
<=> v3_rlvect_1(sK28) ),
introduced(definition,[new_symbols(definition,[spl443_18])],[avatar_definition]) ).
fof(f15872,definition,
( spl443_19
<=> v3_struct_0(sK28) ),
introduced(definition,[new_symbols(definition,[spl443_19])],[avatar_definition]) ).
fof(f15876,definition,
( spl443_20
<=> ! [X0] :
( sF439 = X0
| ~ r1_rlvect_1(sF437,X0) ) ),
introduced(definition,[new_symbols(definition,[spl443_20])],[avatar_definition]) ).
fof(f15877,plain,
( ! [X0] :
( ~ r1_rlvect_1(sF437,X0)
| sF439 = X0 )
| ~ spl443_20 ),
inference(avatar_component_clause,[],[f15876]) ).
fof(f15878,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| spl443_20 ),
inference(avatar_split_clause,[],[f15806,f15876,f15872,f15868,f15864,f15860,f15856,f15852,f15848,f15844,f15840,f15836,f15832,f15828,f15824,f15820,f15816,f15812,f15808]) ).
fof(f15881,plain,
spl443_3,
inference(avatar_split_clause,[],[f12825,f15808]) ).
fof(f15884,plain,
spl443_4,
inference(avatar_split_clause,[],[f12828,f15812]) ).
fof(f15887,plain,
spl443_5,
inference(avatar_split_clause,[],[f12829,f15816]) ).
fof(f15890,plain,
spl443_6,
inference(avatar_split_clause,[],[f12830,f15820]) ).
fof(f15893,plain,
spl443_7,
inference(avatar_split_clause,[],[f12832,f15824]) ).
fof(f15896,plain,
spl443_8,
inference(avatar_split_clause,[],[f12833,f15828]) ).
fof(f15902,definition,
( spl443_21
<=> l1_struct_0(sK28) ),
introduced(definition,[new_symbols(definition,[spl443_21])],[avatar_definition]) ).
fof(f15918,plain,
spl443_9,
inference(avatar_split_clause,[],[f12834,f15832]) ).
fof(f15921,plain,
spl443_10,
inference(avatar_split_clause,[],[f12835,f15836]) ).
fof(f15924,plain,
spl443_11,
inference(avatar_split_clause,[],[f12836,f15840]) ).
fof(f15948,plain,
spl443_15,
inference(avatar_split_clause,[],[f12840,f15856]) ).
fof(f15951,plain,
spl443_16,
inference(avatar_split_clause,[],[f12841,f15860]) ).
fof(f15954,plain,
spl443_17,
inference(avatar_split_clause,[],[f12842,f15864]) ).
fof(f15957,plain,
spl443_18,
inference(avatar_split_clause,[],[f12843,f15868]) ).
fof(f15960,plain,
~ spl443_19,
inference(avatar_split_clause,[],[f12844,f15872]) ).
fof(f15973,plain,
! [X0] :
( r1_rlvect_1(sF438,X0)
| ~ r2_hidden(X0,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK28)))
| v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v7_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| v10_vectsp_1(sK27)
| ~ v2_vectsp_2(sK27)
| ~ l3_vectsp_1(sK27) ),
inference(superposition,[],[f13053,f15768]) ).
fof(f15974,plain,
! [X0] :
( r1_rlvect_1(sF437,X0)
| ~ r2_hidden(X0,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK28)))
| v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v7_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| v10_vectsp_1(sK27)
| ~ v2_vectsp_2(sK27)
| ~ l3_vectsp_1(sK27) ),
inference(forward_demodulation,[],[f15973,f15769]) ).
fof(f15975,plain,
! [X0] :
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF441))
| r1_rlvect_1(sF437,X0)
| ~ r2_hidden(X0,sK29)
| v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v7_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| v10_vectsp_1(sK27)
| ~ v2_vectsp_2(sK27)
| ~ l3_vectsp_1(sK27) ),
inference(forward_demodulation,[],[f15974,f15776]) ).
fof(f15976,plain,
! [X0] :
( ~ m1_subset_1(sK29,sF442)
| r1_rlvect_1(sF437,X0)
| ~ r2_hidden(X0,sK29)
| v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v7_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| v10_vectsp_1(sK27)
| ~ v2_vectsp_2(sK27)
| ~ l3_vectsp_1(sK27) ),
inference(forward_demodulation,[],[f15975,f15778]) ).
fof(f15978,definition,
( spl443_28
<=> v2_vectsp_2(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_28])],[avatar_definition]) ).
fof(f15982,definition,
( spl443_29
<=> v10_vectsp_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_29])],[avatar_definition]) ).
fof(f15986,definition,
( spl443_30
<=> v7_group_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_30])],[avatar_definition]) ).
fof(f15990,definition,
( spl443_31
<=> ! [X0] :
( r1_rlvect_1(sF437,X0)
| ~ r2_hidden(X0,sK29) ) ),
introduced(definition,[new_symbols(definition,[spl443_31])],[avatar_definition]) ).
fof(f15991,plain,
( ! [X0] :
( r1_rlvect_1(sF437,X0)
| ~ r2_hidden(X0,sK29) )
| ~ spl443_31 ),
inference(avatar_component_clause,[],[f15990]) ).
fof(f15993,definition,
( spl443_32
<=> m1_subset_1(sK29,sF442) ),
introduced(definition,[new_symbols(definition,[spl443_32])],[avatar_definition]) ).
fof(f15996,plain,
( ~ spl443_3
| ~ spl443_28
| spl443_29
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_30
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| spl443_31
| ~ spl443_32 ),
inference(avatar_split_clause,[],[f15976,f15993,f15990,f15872,f15868,f15864,f15860,f15856,f15852,f15848,f15844,f15840,f15836,f15832,f15828,f15824,f15986,f15820,f15816,f15812,f15982,f15978,f15808]) ).
fof(f15999,plain,
spl443_13,
inference(avatar_split_clause,[],[f12838,f15848]) ).
fof(f16002,plain,
spl443_14,
inference(avatar_split_clause,[],[f12839,f15852]) ).
fof(f16005,plain,
spl443_32,
inference(avatar_split_clause,[],[f15779,f15993]) ).
fof(f16008,plain,
spl443_28,
inference(avatar_split_clause,[],[f12826,f15978]) ).
fof(f16011,plain,
spl443_30,
inference(avatar_split_clause,[],[f12831,f15986]) ).
fof(f16014,plain,
~ spl443_29,
inference(avatar_split_clause,[],[f12827,f15982]) ).
fof(f16017,plain,
~ spl443_12,
inference(avatar_split_clause,[],[f12837,f15844]) ).
fof(f16018,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK29)
| sF439 = X0 )
| ~ spl443_20
| ~ spl443_31 ),
inference(resolution,[],[f15991,f15877]) ).
fof(f16122,plain,
( sF440 = k1_tarski(sF439)
| v3_struct_0(sK28)
| ~ l1_struct_0(sK28)
| ~ m1_subset_1(sF439,u1_struct_0(sK28)) ),
inference(superposition,[],[f13025,f15773]) ).
fof(f16129,plain,
( ~ m1_subset_1(sF439,sF441)
| sF440 = k1_tarski(sF439)
| v3_struct_0(sK28)
| ~ l1_struct_0(sK28) ),
inference(forward_demodulation,[],[f16122,f15776]) ).
fof(f16131,definition,
( spl443_42
<=> sF440 = k1_tarski(sF439) ),
introduced(definition,[new_symbols(definition,[spl443_42])],[avatar_definition]) ).
fof(f16133,plain,
( sF440 = k1_tarski(sF439)
| ~ spl443_42 ),
inference(avatar_component_clause,[],[f16131]) ).
fof(f16135,plain,
( ~ spl443_21
| spl443_19
| spl443_42
| ~ spl443_2 ),
inference(avatar_split_clause,[],[f16129,f15800,f16131,f15872,f15902]) ).
fof(f16158,plain,
! [X0,X1] :
( ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(sK28,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)
| 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)
| m2_rmod_2(sF441,X0,X1,sK28)
| ~ l3_vectsp_1(X0) ),
inference(superposition,[],[f14036,f15776]) ).
fof(f16170,definition,
( spl443_46
<=> r2_hidden(sF439,sF441) ),
introduced(definition,[new_symbols(definition,[spl443_46])],[avatar_definition]) ).
fof(f16292,plain,
! [X2,X0,X1] :
( sF441 != X0
| r2_hidden(k1_rlvect_1(X1),X0)
| ~ m2_rmod_2(X0,X2,X1,sK28)
| ~ m1_rmod_2(sK28,X2,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,X2)
| ~ l1_vectsp_2(X1,X2)
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v4_group_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v7_vectsp_1(X2)
| ~ v8_vectsp_1(X2)
| ~ l3_vectsp_1(X2) ),
inference(superposition,[],[f14035,f15776]) ).
fof(f16294,plain,
! [X0,X1] :
( ~ m2_rmod_2(sF441,X1,X0,sK28)
| r2_hidden(k1_rlvect_1(X0),sF441)
| ~ m1_rmod_2(sK28,X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,X1)
| ~ l1_vectsp_2(X0,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) ),
inference(equality_resolution,[],[f16292]) ).
fof(f16380,plain,
( ~ r2_hidden(sF439,sF441)
| spl443_2 ),
inference(resolution,[],[f13158,f15801]) ).
fof(f16381,plain,
( ~ spl443_46
| spl443_2 ),
inference(avatar_split_clause,[],[f16380,f15800,f16170]) ).
fof(f16626,plain,
( np__0 = sK29
| sF439 = sK285(sK29)
| ~ spl443_20
| ~ spl443_31 ),
inference(resolution,[],[f15640,f16018]) ).
fof(f16628,definition,
( spl443_88
<=> sF439 = sK285(sK29) ),
introduced(definition,[new_symbols(definition,[spl443_88])],[avatar_definition]) ).
fof(f16630,plain,
( sF439 = sK285(sK29)
| ~ spl443_88 ),
inference(avatar_component_clause,[],[f16628]) ).
fof(f16632,definition,
( spl443_89
<=> np__0 = sK29 ),
introduced(definition,[new_symbols(definition,[spl443_89])],[avatar_definition]) ).
fof(f16635,plain,
( spl443_88
| spl443_89
| ~ spl443_20
| ~ spl443_31 ),
inference(avatar_split_clause,[],[f16626,f15990,f15876,f16632,f16628]) ).
fof(f16636,plain,
( r2_hidden(sF439,sK29)
| np__0 = sK29
| ~ spl443_88 ),
inference(superposition,[],[f15640,f16630]) ).
fof(f16638,definition,
( spl443_90
<=> r2_hidden(sF439,sK29) ),
introduced(definition,[new_symbols(definition,[spl443_90])],[avatar_definition]) ).
fof(f16641,plain,
( spl443_89
| spl443_90
| ~ spl443_88 ),
inference(avatar_split_clause,[],[f16636,f16628,f16638,f16632]) ).
fof(f16649,plain,
~ spl443_89,
inference(avatar_split_clause,[],[f15418,f16632]) ).
fof(f16741,definition,
( spl443_97
<=> m1_rmod_2(sK28,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl443_97])],[avatar_definition]) ).
fof(f16743,plain,
( ~ m1_rmod_2(sK28,sK27,sK28)
| spl443_97 ),
inference(avatar_component_clause,[],[f16741]) ).
fof(f16822,definition,
( spl443_111
<=> k1_rlvect_1(sK27) = k2_group_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_111])],[avatar_definition]) ).
fof(f16823,plain,
( k1_rlvect_1(sK27) != k2_group_1(sK27)
| spl443_111 ),
inference(avatar_component_clause,[],[f16822]) ).
fof(f16824,plain,
( k1_rlvect_1(sK27) = k2_group_1(sK27)
| ~ spl443_111 ),
inference(avatar_component_clause,[],[f16822]) ).
fof(f16829,plain,
( k1_rlvect_1(sK27) != k1_rlvect_1(sK27)
| v10_vectsp_1(sK27)
| v3_struct_0(sK27)
| ~ l2_vectsp_1(sK27)
| ~ spl443_111 ),
inference(superposition,[],[f13446,f16824]) ).
fof(f16830,plain,
( v10_vectsp_1(sK27)
| v3_struct_0(sK27)
| ~ l2_vectsp_1(sK27)
| ~ spl443_111 ),
inference(trivial_inequality_removal,[],[f16829]) ).
fof(f16832,definition,
( spl443_113
<=> l2_vectsp_1(sK27) ),
introduced(definition,[new_symbols(definition,[spl443_113])],[avatar_definition]) ).
fof(f16833,plain,
( l2_vectsp_1(sK27)
| ~ spl443_113 ),
inference(avatar_component_clause,[],[f16832]) ).
fof(f16834,plain,
( ~ l2_vectsp_1(sK27)
| spl443_113 ),
inference(avatar_component_clause,[],[f16832]) ).
fof(f16835,plain,
( ~ spl443_113
| spl443_12
| spl443_29
| ~ spl443_111 ),
inference(avatar_split_clause,[],[f16830,f16822,f15982,f15844,f16832]) ).
fof(f16836,plain,
( ~ l3_vectsp_1(sK27)
| spl443_113 ),
inference(resolution,[],[f16834,f13440]) ).
fof(f16837,plain,
( ~ spl443_3
| spl443_113 ),
inference(avatar_split_clause,[],[f16836,f16832,f15808]) ).
fof(f16863,plain,
( ! [X0] :
( ~ m1_rmod_2(sK28,sK27,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK27)
| ~ l1_vectsp_2(X0,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| m2_rmod_2(sF441,sK27,X0,sK28)
| ~ l3_vectsp_1(sK27) )
| ~ spl443_4 ),
inference(resolution,[],[f16158,f15813]) ).
fof(f16865,definition,
( spl443_118
<=> ! [X0] :
( ~ m1_rmod_2(sK28,sK27,X0)
| m2_rmod_2(sF441,sK27,X0,sK28)
| ~ l1_vectsp_2(X0,sK27)
| ~ v5_vectsp_2(X0,sK27)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl443_118])],[avatar_definition]) ).
fof(f16866,plain,
( ! [X0] :
( ~ v5_vectsp_2(X0,sK27)
| m2_rmod_2(sF441,sK27,X0,sK28)
| ~ l1_vectsp_2(X0,sK27)
| ~ m1_rmod_2(sK28,sK27,X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) )
| ~ spl443_118 ),
inference(avatar_component_clause,[],[f16865]) ).
fof(f16867,plain,
( ~ spl443_3
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| spl443_118
| ~ spl443_4 ),
inference(avatar_split_clause,[],[f16863,f15812,f16865,f15844,f15840,f15836,f15832,f15828,f15824,f15820,f15816,f15808]) ).
fof(f16873,plain,
! [X0] : np__0 = k2_zfmisc_1(X0,np__0),
inference(equality_resolution,[],[f15468]) ).
fof(f16920,plain,
( l2_struct_0(sK27)
| ~ spl443_113 ),
inference(resolution,[],[f13443,f16833]) ).
fof(f16921,plain,
( l1_struct_0(sK27)
| ~ spl443_113 ),
inference(resolution,[],[f16920,f14461]) ).
fof(f17400,definition,
( spl443_185
<=> l1_rlvect_1(sK28) ),
introduced(definition,[new_symbols(definition,[spl443_185])],[avatar_definition]) ).
fof(f17402,plain,
( ~ l1_rlvect_1(sK28)
| spl443_185 ),
inference(avatar_component_clause,[],[f17400]) ).
fof(f17565,plain,
( m2_rmod_2(sF441,sK27,sK28,sK28)
| ~ l1_vectsp_2(sK28,sK27)
| ~ m1_rmod_2(sK28,sK27,sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v3_rlvect_1(sK28)
| v3_struct_0(sK28)
| ~ spl443_14
| ~ spl443_118 ),
inference(resolution,[],[f16866,f15853]) ).
fof(f17567,definition,
( spl443_211
<=> m2_rmod_2(sF441,sK27,sK28,sK28) ),
introduced(definition,[new_symbols(definition,[spl443_211])],[avatar_definition]) ).
fof(f17569,plain,
( m2_rmod_2(sF441,sK27,sK28,sK28)
| ~ spl443_211 ),
inference(avatar_component_clause,[],[f17567]) ).
fof(f17570,plain,
( spl443_19
| ~ spl443_18
| ~ spl443_17
| ~ spl443_16
| ~ spl443_15
| ~ spl443_97
| ~ spl443_13
| spl443_211
| ~ spl443_14
| ~ spl443_118 ),
inference(avatar_split_clause,[],[f17565,f16865,f15852,f17567,f15848,f16741,f15856,f15860,f15864,f15868,f15872]) ).
fof(f17571,plain,
( v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| ~ l3_vectsp_1(sK27)
| spl443_97 ),
inference(resolution,[],[f16743,f13654]) ).
fof(f17578,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| spl443_97 ),
inference(avatar_split_clause,[],[f17571,f16741,f15872,f15868,f15864,f15860,f15856,f15852,f15848,f15844,f15840,f15836,f15832,f15828,f15824,f15820,f15816,f15812,f15808]) ).
fof(f17586,plain,
( r2_hidden(k1_rlvect_1(sK28),sF441)
| ~ m1_rmod_2(sK28,sK27,sK28)
| v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| ~ l3_vectsp_1(sK27)
| ~ spl443_211 ),
inference(resolution,[],[f17569,f16294]) ).
fof(f17587,plain,
( r2_hidden(sF439,sF441)
| ~ m1_rmod_2(sK28,sK27,sK28)
| v3_struct_0(sK28)
| ~ v3_rlvect_1(sK28)
| ~ v4_rlvect_1(sK28)
| ~ v5_rlvect_1(sK28)
| ~ v6_rlvect_1(sK28)
| ~ v5_vectsp_2(sK28,sK27)
| ~ l1_vectsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v3_rlvect_1(sK27)
| ~ v4_rlvect_1(sK27)
| ~ v5_rlvect_1(sK27)
| ~ v6_rlvect_1(sK27)
| ~ v4_group_1(sK27)
| ~ v6_vectsp_1(sK27)
| ~ v7_vectsp_1(sK27)
| ~ v8_vectsp_1(sK27)
| ~ l3_vectsp_1(sK27)
| ~ spl443_211 ),
inference(forward_demodulation,[],[f17586,f15771]) ).
fof(f17662,plain,
( ! [X0] :
( ~ l1_struct_0(X0)
| ~ l1_vectsp_2(sK28,X0) )
| spl443_185 ),
inference(resolution,[],[f13764,f17402]) ).
fof(f17663,plain,
( ~ l1_vectsp_2(sK28,sK27)
| ~ spl443_113
| spl443_185 ),
inference(resolution,[],[f17662,f16921]) ).
fof(f17664,plain,
( ~ spl443_13
| ~ spl443_113
| spl443_185 ),
inference(avatar_split_clause,[],[f17663,f17400,f16832,f15848]) ).
fof(f17723,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k1_tarski(X1))
| X0 = X1 ),
inference(equality_resolution,[],[f13759]) ).
fof(f17733,plain,
( ~ l1_rlvect_1(sK28)
| spl443_1 ),
inference(resolution,[],[f14457,f15798]) ).
fof(f17735,plain,
( ~ spl443_185
| spl443_1 ),
inference(avatar_split_clause,[],[f17733,f15796,f17400]) ).
fof(f17736,plain,
( l1_struct_0(sK28)
| ~ spl443_1 ),
inference(resolution,[],[f15797,f14461]) ).
fof(f17737,plain,
( spl443_21
| ~ spl443_1 ),
inference(avatar_split_clause,[],[f17736,f15796,f15902]) ).
fof(f17738,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF440)
| sF439 = X0 )
| ~ spl443_42 ),
inference(superposition,[],[f17723,f16133]) ).
fof(f17774,definition,
( spl443_232
<=> np__0 = sF440 ),
introduced(definition,[new_symbols(definition,[spl443_232])],[avatar_definition]) ).
fof(f17776,plain,
( np__0 = sF440
| ~ spl443_232 ),
inference(avatar_component_clause,[],[f17774]) ).
fof(f18050,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| ~ spl443_97
| spl443_46
| ~ spl443_211 ),
inference(avatar_split_clause,[],[f17587,f17567,f16170,f16741,f15872,f15868,f15864,f15860,f15856,f15852,f15848,f15844,f15840,f15836,f15832,f15828,f15824,f15820,f15816,f15812,f15808]) ).
fof(f21702,plain,
( ! [X0] :
( sF439 = sK72(X0,sK29)
| r2_hidden(sK72(X0,sK29),X0)
| sK29 = X0 )
| ~ spl443_20
| ~ spl443_31 ),
inference(resolution,[],[f13166,f16018]) ).
fof(f21705,plain,
( ! [X0] :
( ~ r2_hidden(sF439,sK29)
| sK29 = X0
| ~ r2_hidden(sF439,X0)
| r2_hidden(sK72(X0,sK29),X0)
| sK29 = X0 )
| ~ spl443_20
| ~ spl443_31 ),
inference(superposition,[],[f13167,f21702]) ).
fof(f21706,plain,
( ! [X0] :
( ~ r2_hidden(sF439,sK29)
| sK29 = X0
| ~ r2_hidden(sF439,X0)
| r2_hidden(sK72(X0,sK29),X0) )
| ~ spl443_20
| ~ spl443_31 ),
inference(duplicate_literal_removal,[],[f21705]) ).
fof(f21709,definition,
( spl443_747
<=> ! [X0] :
( sK29 = X0
| r2_hidden(sK72(X0,sK29),X0)
| ~ r2_hidden(sF439,X0) ) ),
introduced(definition,[new_symbols(definition,[spl443_747])],[avatar_definition]) ).
fof(f21710,plain,
( ! [X0] :
( r2_hidden(sK72(X0,sK29),X0)
| sK29 = X0
| ~ r2_hidden(sF439,X0) )
| ~ spl443_747 ),
inference(avatar_component_clause,[],[f21709]) ).
fof(f21711,plain,
( spl443_747
| ~ spl443_90
| ~ spl443_20
| ~ spl443_31 ),
inference(avatar_split_clause,[],[f21706,f15990,f15876,f16638,f21709]) ).
fof(f22219,plain,
( ! [X0] :
( np__0 != k2_zfmisc_1(X0,sF440)
| np__0 = X0 )
| ~ spl443_42 ),
inference(superposition,[],[f15514,f16133]) ).
fof(f22220,plain,
( ! [X0] :
( np__0 != k2_zfmisc_1(X0,np__0)
| np__0 = X0 )
| ~ spl443_42
| ~ spl443_232 ),
inference(forward_demodulation,[],[f22219,f17776]) ).
fof(f22221,plain,
( ! [X0] :
( np__0 != np__0
| np__0 = X0 )
| ~ spl443_42
| ~ spl443_232 ),
inference(forward_demodulation,[],[f22220,f16873]) ).
fof(f22222,plain,
( ! [X0] : np__0 = X0
| ~ spl443_42
| ~ spl443_232 ),
inference(trivial_inequality_removal,[],[f22221]) ).
fof(f22606,plain,
( k1_rlvect_1(np__0) != k2_group_1(np__0)
| ~ spl443_42
| spl443_111
| ~ spl443_232 ),
inference(superposition,[],[f16823,f22222]) ).
fof(f23685,plain,
( np__0 != k1_rlvect_1(np__0)
| ~ spl443_42
| spl443_111
| ~ spl443_232 ),
inference(forward_demodulation,[],[f22606,f22222]) ).
fof(f24143,plain,
( np__0 != np__0
| ~ spl443_42
| spl443_111
| ~ spl443_232 ),
inference(forward_demodulation,[],[f23685,f22222]) ).
fof(f24144,plain,
( $false
| ~ spl443_42
| spl443_111
| ~ spl443_232 ),
inference(trivial_inequality_removal,[],[f24143]) ).
fof(f24145,plain,
( ~ spl443_42
| spl443_111
| ~ spl443_232 ),
inference(avatar_contradiction_clause,[],[f24144]) ).
fof(f24847,plain,
( ! [X0] :
( sF439 = sK70(sF440,X0)
| r1_tarski(sF440,X0) )
| ~ spl443_42 ),
inference(resolution,[],[f17738,f13151]) ).
fof(f24849,plain,
( sF439 = sK72(sF440,sK29)
| sK29 = sF440
| ~ r2_hidden(sF439,sF440)
| ~ spl443_42
| ~ spl443_747 ),
inference(resolution,[],[f17738,f21710]) ).
fof(f24869,definition,
( spl443_859
<=> r2_hidden(sF439,sF440) ),
introduced(definition,[new_symbols(definition,[spl443_859])],[avatar_definition]) ).
fof(f24873,definition,
( spl443_860
<=> sK29 = sF440 ),
introduced(definition,[new_symbols(definition,[spl443_860])],[avatar_definition]) ).
fof(f24877,definition,
( spl443_861
<=> sF439 = sK72(sF440,sK29) ),
introduced(definition,[new_symbols(definition,[spl443_861])],[avatar_definition]) ).
fof(f24879,plain,
( sF439 = sK72(sF440,sK29)
| ~ spl443_861 ),
inference(avatar_component_clause,[],[f24877]) ).
fof(f24880,plain,
( ~ spl443_859
| spl443_860
| spl443_861
| ~ spl443_42
| ~ spl443_747 ),
inference(avatar_split_clause,[],[f24849,f21709,f16131,f24877,f24873,f24869]) ).
fof(f24894,plain,
( ! [X0] :
( r2_hidden(sF439,sF440)
| r1_tarski(sF440,X0)
| r1_tarski(sF440,X0) )
| ~ spl443_42 ),
inference(superposition,[],[f13151,f24847]) ).
fof(f24897,plain,
( ! [X0] :
( r2_hidden(sF439,sF440)
| r1_tarski(sF440,X0) )
| ~ spl443_42 ),
inference(duplicate_literal_removal,[],[f24894]) ).
fof(f24899,definition,
( spl443_865
<=> ! [X0] : r1_tarski(sF440,X0) ),
introduced(definition,[new_symbols(definition,[spl443_865])],[avatar_definition]) ).
fof(f24900,plain,
( ! [X0] : r1_tarski(sF440,X0)
| ~ spl443_865 ),
inference(avatar_component_clause,[],[f24899]) ).
fof(f24901,plain,
( spl443_865
| spl443_859
| ~ spl443_42 ),
inference(avatar_split_clause,[],[f24897,f16131,f24869,f24899]) ).
fof(f24910,plain,
( np__0 = sF440
| ~ spl443_865 ),
inference(resolution,[],[f24900,f15470]) ).
fof(f24931,plain,
( spl443_232
| ~ spl443_865 ),
inference(avatar_split_clause,[],[f24910,f24899,f17774]) ).
fof(f24940,plain,
~ spl443_860,
inference(avatar_split_clause,[],[f15774,f24873]) ).
fof(f24943,plain,
( ~ r2_hidden(sF439,sK29)
| sK29 = sF440
| ~ r2_hidden(sF439,sF440)
| ~ spl443_861 ),
inference(superposition,[],[f13167,f24879]) ).
fof(f24944,plain,
( ~ spl443_859
| spl443_860
| ~ spl443_90
| ~ spl443_861 ),
inference(avatar_split_clause,[],[f24943,f24877,f16638,f24873,f24869]) ).
cnf(s3,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| spl443_20 ),
inference(sat_conversion,[],[f15878]) ).
cnf(s5,plain,
spl443_3,
inference(sat_conversion,[],[f15881]) ).
cnf(s7,plain,
spl443_4,
inference(sat_conversion,[],[f15884]) ).
cnf(s9,plain,
spl443_5,
inference(sat_conversion,[],[f15887]) ).
cnf(s11,plain,
spl443_6,
inference(sat_conversion,[],[f15890]) ).
cnf(s13,plain,
spl443_7,
inference(sat_conversion,[],[f15893]) ).
cnf(s15,plain,
spl443_8,
inference(sat_conversion,[],[f15896]) ).
cnf(s19,plain,
spl443_9,
inference(sat_conversion,[],[f15918]) ).
cnf(s21,plain,
spl443_10,
inference(sat_conversion,[],[f15921]) ).
cnf(s23,plain,
spl443_11,
inference(sat_conversion,[],[f15924]) ).
cnf(s28,plain,
spl443_15,
inference(sat_conversion,[],[f15948]) ).
cnf(s30,plain,
spl443_16,
inference(sat_conversion,[],[f15951]) ).
cnf(s32,plain,
spl443_17,
inference(sat_conversion,[],[f15954]) ).
cnf(s34,plain,
spl443_18,
inference(sat_conversion,[],[f15957]) ).
cnf(s36,plain,
~ spl443_19,
inference(sat_conversion,[],[f15960]) ).
cnf(s39,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| ~ spl443_28
| spl443_29
| ~ spl443_30
| spl443_31
| ~ spl443_32 ),
inference(sat_conversion,[],[f15996]) ).
cnf(s41,plain,
spl443_13,
inference(sat_conversion,[],[f15999]) ).
cnf(s43,plain,
spl443_14,
inference(sat_conversion,[],[f16002]) ).
cnf(s45,plain,
spl443_32,
inference(sat_conversion,[],[f16005]) ).
cnf(s47,plain,
spl443_28,
inference(sat_conversion,[],[f16008]) ).
cnf(s49,plain,
spl443_30,
inference(sat_conversion,[],[f16011]) ).
cnf(s51,plain,
~ spl443_29,
inference(sat_conversion,[],[f16014]) ).
cnf(s53,plain,
~ spl443_12,
inference(sat_conversion,[],[f16017]) ).
cnf(s65,plain,
( ~ spl443_2
| spl443_19
| ~ spl443_21
| spl443_42 ),
inference(sat_conversion,[],[f16135]) ).
cnf(s87,plain,
( spl443_2
| ~ spl443_46 ),
inference(sat_conversion,[],[f16381]) ).
cnf(s104,plain,
( ~ spl443_20
| ~ spl443_31
| spl443_88
| spl443_89 ),
inference(sat_conversion,[],[f16635]) ).
cnf(s105,plain,
( ~ spl443_88
| spl443_89
| spl443_90 ),
inference(sat_conversion,[],[f16641]) ).
cnf(s107,plain,
~ spl443_89,
inference(sat_conversion,[],[f16649]) ).
cnf(s130,plain,
( spl443_12
| spl443_29
| ~ spl443_111
| ~ spl443_113 ),
inference(sat_conversion,[],[f16835]) ).
cnf(s131,plain,
( ~ spl443_3
| spl443_113 ),
inference(sat_conversion,[],[f16837]) ).
cnf(s136,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| spl443_118 ),
inference(sat_conversion,[],[f16867]) ).
cnf(s227,plain,
( ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| ~ spl443_97
| ~ spl443_118
| spl443_211 ),
inference(sat_conversion,[],[f17570]) ).
cnf(s229,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| spl443_97 ),
inference(sat_conversion,[],[f17578]) ).
cnf(s239,plain,
( ~ spl443_13
| ~ spl443_113
| spl443_185 ),
inference(sat_conversion,[],[f17664]) ).
cnf(s246,plain,
( spl443_1
| ~ spl443_185 ),
inference(sat_conversion,[],[f17735]) ).
cnf(s247,plain,
( ~ spl443_1
| spl443_21 ),
inference(sat_conversion,[],[f17737]) ).
cnf(s285,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| spl443_12
| ~ spl443_13
| ~ spl443_14
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| spl443_46
| ~ spl443_97
| ~ spl443_211 ),
inference(sat_conversion,[],[f18050]) ).
cnf(s783,plain,
( ~ spl443_20
| ~ spl443_31
| ~ spl443_90
| spl443_747 ),
inference(sat_conversion,[],[f21711]) ).
cnf(s857,plain,
( ~ spl443_42
| spl443_111
| ~ spl443_232 ),
inference(sat_conversion,[],[f24145]) ).
cnf(s986,plain,
( ~ spl443_42
| ~ spl443_747
| ~ spl443_859
| spl443_860
| spl443_861 ),
inference(sat_conversion,[],[f24880]) ).
cnf(s990,plain,
( ~ spl443_42
| spl443_859
| spl443_865 ),
inference(sat_conversion,[],[f24901]) ).
cnf(s995,plain,
( spl443_232
| ~ spl443_865 ),
inference(sat_conversion,[],[f24931]) ).
cnf(s999,plain,
~ spl443_860,
inference(sat_conversion,[],[f24940]) ).
cnf(s1000,plain,
( ~ spl443_90
| ~ spl443_859
| spl443_860
| ~ spl443_861 ),
inference(sat_conversion,[],[f24944]) ).
cnf(s1001,plain,
( ~ spl443_42
| ~ spl443_747
| ~ spl443_859
| spl443_861 ),
inference(rat,[],[s986,s999]) ).
cnf(s1007,plain,
( ~ spl443_88
| spl443_90 ),
inference(rat,[],[s105,s107]) ).
cnf(s1008,plain,
( ~ spl443_20
| ~ spl443_31
| spl443_88 ),
inference(rat,[],[s104,s107]) ).
cnf(s1013,plain,
( ~ spl443_3
| ~ spl443_4
| ~ spl443_5
| ~ spl443_6
| ~ spl443_7
| ~ spl443_8
| ~ spl443_9
| ~ spl443_10
| ~ spl443_11
| ~ spl443_15
| ~ spl443_16
| ~ spl443_17
| ~ spl443_18
| spl443_19
| spl443_31 ),
inference(rat,[],[s39,s45,s49,s51,s47,s43,s41,s53]) ).
cnf(s1142,plain,
spl443_97,
inference(rat,[],[s229,s7,s36,s34,s32,s30,s28,s43,s41,s53,s23,s21,s19,s15,s13,s11,s9,s5]) ).
cnf(s1169,plain,
spl443_118,
inference(rat,[],[s136,s7,s53,s23,s21,s19,s15,s13,s11,s9,s5]) ).
cnf(s1173,plain,
spl443_113,
inference(rat,[],[s131,s5]) ).
cnf(s1186,plain,
spl443_31,
inference(rat,[],[s1013,s7,s36,s34,s32,s30,s28,s23,s21,s19,s15,s13,s11,s9,s5]) ).
cnf(s1265,plain,
spl443_211,
inference(rat,[],[s227,s1142,s28,s30,s36,s34,s32,s41,s43,s1169]) ).
cnf(s1270,plain,
spl443_185,
inference(rat,[],[s239,s41,s1173]) ).
cnf(s1273,plain,
~ spl443_111,
inference(rat,[],[s130,s51,s53,s1173]) ).
cnf(s1353,plain,
spl443_46,
inference(rat,[],[s285,s1142,s5,s7,s36,s34,s32,s30,s28,s43,s41,s53,s23,s21,s19,s15,s13,s11,s9,s1265]) ).
cnf(s1354,plain,
spl443_1,
inference(rat,[],[s246,s1270]) ).
cnf(s1394,plain,
spl443_2,
inference(rat,[],[s87,s1353]) ).
cnf(s1397,plain,
spl443_21,
inference(rat,[],[s247,s1354]) ).
cnf(s1465,plain,
spl443_42,
inference(rat,[],[s65,s1394,s36,s1397]) ).
cnf(s1512,plain,
~ spl443_232,
inference(rat,[],[s857,s1273,s1465]) ).
cnf(s1521,plain,
~ spl443_865,
inference(rat,[],[s995,s1512]) ).
cnf(s1530,plain,
spl443_859,
inference(rat,[],[s990,s1465,s1521]) ).
cnf(s1531,plain,
spl443_20,
inference(rat,[],[s3,s36,s34,s32,s30,s28,s43,s41,s53,s23,s21,s19,s15,s13,s11,s9,s7,s5]) ).
cnf(s1545,plain,
spl443_88,
inference(rat,[],[s1008,s1186,s1531]) ).
cnf(s1562,plain,
spl443_90,
inference(rat,[],[s1007,s1545]) ).
cnf(s1580,plain,
~ spl443_861,
inference(rat,[],[s1000,s1530,s999,s1562]) ).
cnf(s1581,plain,
spl443_747,
inference(rat,[],[s783,s1531,s1186,s1562]) ).
cnf(s1592,plain,
$false,
inference(rat,[],[s1001,s1530,s1465,s1580,s1581]) ).
fof(f24945,plain,
$false,
inference(avatar_sat_refutation,[],[s1592]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG218+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n019.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:46:20 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.25/3.35 % (163519)Detected formulas, will run a generic FOF schedule.
% 16.25/3.35 % (163524)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=3930251438:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 16.25/3.35 % (163530)dis-21_1_sil=8000:lcm=predicate:random_seed=3082302063: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)
% 16.25/3.35 % (163526)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=2884753277:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 16.25/3.35 % (163527)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=11157844:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 16.25/3.35 % (163528)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3093703976:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 16.25/3.35 % (163525)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=3735652454:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 16.25/3.35 % (163529)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3970571182:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 16.25/3.35 % (163529)Instruction limit reached!
% 16.25/3.35 % (163529)------------------------------
% 16.25/3.35 % (163529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.25/3.35 % (163529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.25/3.35 % (163529)CaDiCaL version: 2.1.3
% 16.25/3.35 % (163529)Termination reason: Instruction limit
% 16.25/3.35 % (163529)Termination phase: SInE selection
% 16.25/3.35 % (163529)Time elapsed: 0.066 s
% 16.25/3.35 % (163529)Peak memory usage: 97 MB
% 16.25/3.35 % (163529)Instructions burned: 140 (million)
% 16.25/3.35 % (163527)Instruction limit reached!
% 16.25/3.35 % (163527)------------------------------
% 16.25/3.35 % (163527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.25/3.35 % (163527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.25/3.35 % (163527)CaDiCaL version: 2.1.3
% 16.25/3.35 % (163527)Termination reason: Instruction limit
% 16.25/3.35 % (163527)Termination phase: Saturation
% 16.25/3.35 % (163527)Time elapsed: 0.071 s
% 16.25/3.35 % (163527)Peak memory usage: 101 MB
% 16.25/3.35 % (163527)Instructions burned: 109 (million)
% 16.25/3.35 % (163528)Instruction limit reached!
% 16.25/3.35 % (163528)------------------------------
% 16.25/3.35 % (163528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.25/3.35 % (163528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.25/3.35 % (163528)CaDiCaL version: 2.1.3
% 16.25/3.35 % (163528)Termination reason: Instruction limit
% 16.25/3.35 % (163528)Termination phase: Preprocessing 3
% 16.25/3.35 % (163528)Time elapsed: 0.089 s
% 16.25/3.35 % (163528)Peak memory usage: 100 MB
% 16.25/3.35 % (163528)Instructions burned: 119 (million)
% 16.25/3.35 % (163530)Instruction limit reached!
% 16.25/3.35 % (163530)------------------------------
% 16.25/3.35 % (163530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.25/3.35 % (163530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.25/3.35 % (163530)CaDiCaL version: 2.1.3
% 16.25/3.35 % (163530)Termination reason: Instruction limit
% 16.25/3.35 % (163530)Termination phase: Unused predicate definition removal
% 16.25/3.35 % (163530)Time elapsed: 0.097 s
% 16.25/3.35 % (163530)Peak memory usage: 98 MB
% 16.25/3.35 % (163530)Instructions burned: 129 (million)
% 16.25/3.35 % (163538)lrs+10_1_sil=8000:sp=occurrence:random_seed=3910086301:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 16.25/3.35 % (163539)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4054723323:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 16.25/3.35 % (163540)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2488228433:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi)
% 16.25/3.35 % (163541)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=1839491012:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 16.25/3.35 % (163539)Instruction limit reached!
% 16.25/3.35 % (163539)------------------------------
% 23.22/4.32 % (163539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.32 % (163539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.32 % (163539)CaDiCaL version: 2.1.3
% 23.22/4.32 % (163539)Termination reason: Instruction limit
% 23.22/4.32 % (163539)Termination phase: SInE selection
% 23.22/4.32 % (163539)Time elapsed: 0.079 s
% 23.22/4.32 % (163539)Peak memory usage: 97 MB
% 23.22/4.32 % (163539)Instructions burned: 157 (million)
% 23.22/4.32 % (163538)Instruction limit reached!
% 23.22/4.32 % (163538)------------------------------
% 23.22/4.32 % (163538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.32 % (163538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.32 % (163538)CaDiCaL version: 2.1.3
% 23.22/4.32 % (163538)Termination reason: Instruction limit
% 23.22/4.32 % (163538)Termination phase: Saturation
% 23.22/4.32 % (163538)Time elapsed: 0.157 s
% 23.22/4.32 % (163538)Peak memory usage: 104 MB
% 23.22/4.32 % (163538)Instructions burned: 286 (million)
% 23.22/4.32 % (163541)Instruction limit reached!
% 23.22/4.32 % (163541)------------------------------
% 23.22/4.32 % (163541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.32 % (163541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.32 % (163541)CaDiCaL version: 2.1.3
% 23.22/4.32 % (163541)Termination reason: Instruction limit
% 23.22/4.32 % (163541)Termination phase: Preprocessing 1
% 23.22/4.32 % (163541)Time elapsed: 0.137 s
% 23.22/4.32 % (163541)Peak memory usage: 97 MB
% 23.22/4.32 % (163541)Instructions burned: 248 (million)
% 23.22/4.32 % (163540)Instruction limit reached!
% 23.22/4.32 % (163540)------------------------------
% 23.22/4.32 % (163540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.32 % (163540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.32 % (163540)CaDiCaL version: 2.1.3
% 23.22/4.32 % (163540)Termination reason: Instruction limit
% 23.22/4.32 % (163540)Termination phase: Saturation
% 23.22/4.32 % (163540)Time elapsed: 0.203 s
% 23.22/4.32 % (163540)Peak memory usage: 103 MB
% 23.22/4.32 % (163540)Instructions burned: 325 (million)
% 23.22/4.32 % (163546)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2527390289:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 23.22/4.32 % (163547)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1833603055:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 23.22/4.32 % (163548)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1013499448:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 23.22/4.32 % (163548)Instruction limit reached!
% 23.22/4.32 % (163548)------------------------------
% 23.22/4.32 % (163548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.32 % (163548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.32 % (163548)CaDiCaL version: 2.1.3
% 23.22/4.32 % (163548)Termination reason: Instruction limit
% 23.22/4.32 % (163548)Termination phase: Preprocessing 3
% 23.22/4.32 % (163548)Time elapsed: 0.089 s
% 23.22/4.32 % (163548)Peak memory usage: 100 MB
% 23.22/4.32 % (163548)Instructions burned: 114 (million)
% 23.22/4.32 % (163549)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=844978455:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 23.22/4.32 % (163546)Instruction limit reached!
% 23.22/4.32 % (163546)------------------------------
% 23.22/4.32 % (163546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.32 % (163546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.32 % (163546)CaDiCaL version: 2.1.3
% 23.22/4.32 % (163546)Termination reason: Instruction limit
% 23.22/4.32 % (163546)Termination phase: Saturation
% 23.22/4.32 % (163546)Time elapsed: 0.176 s
% 23.22/4.32 % (163546)Peak memory usage: 105 MB
% 23.22/4.32 % (163546)Instructions burned: 294 (million)
% 23.22/4.32 % (163549)Instruction limit reached!
% 23.22/4.32 % (163549)------------------------------
% 23.22/4.32 % (163549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.32 % (163549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.32 % (163549)CaDiCaL version: 2.1.3
% 23.22/4.32 % (163549)Termination reason: Instruction limit
% 23.22/4.32 % (163549)Termination phase: Naming
% 23.22/4.32 % (163549)Time elapsed: 0.101 s
% 23.22/4.32 % (163549)Peak memory usage: 106 MB
% 57.77/9.15 % (163549)Instructions burned: 128 (million)
% 57.77/9.15 % (163554)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4145721692:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 57.77/9.15 % (163555)lrs+10_1_sil=8000:sp=occurrence:random_seed=3405760896:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 57.77/9.15 % (163554)Instruction limit reached!
% 57.77/9.15 % (163554)------------------------------
% 57.77/9.15 % (163554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.77/9.15 % (163554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.77/9.15 % (163554)CaDiCaL version: 2.1.3
% 57.77/9.15 % (163554)Termination reason: Instruction limit
% 57.77/9.15 % (163554)Termination phase: Property scanning
% 57.77/9.15 % (163554)Time elapsed: 0.049 s
% 57.77/9.15 % (163554)Peak memory usage: 96 MB
% 57.77/9.15 % (163554)Instructions burned: 116 (million)
% 57.77/9.15 % (163556)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4230653224:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 57.77/9.15 % (163559)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1957554187:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 57.77/9.15 % (163556)Instruction limit reached!
% 57.77/9.15 % (163556)------------------------------
% 57.77/9.15 % (163556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.77/9.15 % (163556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.77/9.15 % (163556)CaDiCaL version: 2.1.3
% 57.77/9.15 % (163556)Termination reason: Instruction limit
% 57.77/9.15 % (163556)Termination phase: Saturation
% 57.77/9.15 % (163556)Time elapsed: 0.228 s
% 57.77/9.15 % (163556)Peak memory usage: 103 MB
% 57.77/9.15 % (163556)Instructions burned: 438 (million)
% 57.77/9.15 % (163562)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=303348756:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 57.77/9.15 % (163555)Instruction limit reached!
% 57.77/9.15 % (163555)------------------------------
% 57.77/9.15 % (163555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.77/9.15 % (163555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.77/9.15 % (163555)CaDiCaL version: 2.1.3
% 57.77/9.15 % (163555)Termination reason: Instruction limit
% 57.77/9.15 % (163555)Termination phase: Saturation
% 57.77/9.15 % (163555)Time elapsed: 0.512 s
% 57.77/9.15 % (163555)Peak memory usage: 116 MB
% 57.77/9.15 % (163555)Instructions burned: 907 (million)
% 57.77/9.15 % (163562)Instruction limit reached!
% 57.77/9.15 % (163562)------------------------------
% 57.77/9.15 % (163562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.77/9.15 % (163562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.77/9.15 % (163562)CaDiCaL version: 2.1.3
% 57.77/9.15 % (163562)Termination reason: Instruction limit
% 57.77/9.15 % (163562)Termination phase: Saturation
% 57.77/9.15 % (163562)Time elapsed: 0.091 s
% 57.77/9.15 % (163562)Peak memory usage: 102 MB
% 57.77/9.15 % (163562)Instructions burned: 135 (million)
% 57.77/9.15 % (163564)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2656909634:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 57.77/9.15 % (163565)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3071103603:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 57.77/9.15 % (163564)Instruction limit reached!
% 57.77/9.15 % (163564)------------------------------
% 57.77/9.15 % (163564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.77/9.15 % (163564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.77/9.15 % (163564)CaDiCaL version: 2.1.3
% 57.77/9.15 % (163564)Termination reason: Instruction limit
% 57.77/9.15 % (163564)Termination phase: Equality resolution with deletion
% 57.77/9.15 % (163564)Time elapsed: 0.354 s
% 57.77/9.15 % (163564)Peak memory usage: 114 MB
% 57.77/9.15 % (163564)Instructions burned: 593 (million)
% 57.77/9.15 % (163568)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=1696803780:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/125Mi)
% 57.77/9.15 % (163568)Instruction limit reached!
% 57.77/9.15 % (163568)------------------------------
% 81.17/12.57 % (163568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.17/12.57 % (163568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.17/12.57 % (163568)CaDiCaL version: 2.1.3
% 81.17/12.57 % (163568)Termination reason: Instruction limit
% 81.17/12.57 % (163568)Termination phase: SInE selection
% 81.17/12.57 % (163568)Time elapsed: 0.059 s
% 81.17/12.57 % (163568)Peak memory usage: 97 MB
% 81.17/12.57 % (163568)Instructions burned: 125 (million)
% 81.17/12.57 % (163547)Instruction limit reached!
% 81.17/12.57 % (163547)------------------------------
% 81.17/12.57 % (163547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.17/12.57 % (163547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.17/12.57 % (163547)CaDiCaL version: 2.1.3
% 81.17/12.57 % (163547)Termination reason: Instruction limit
% 81.17/12.57 % (163547)Termination phase: Saturation
% 81.17/12.57 % (163547)Time elapsed: 1.680 s
% 81.17/12.57 % (163547)Peak memory usage: 317 MB
% 81.17/12.57 % (163547)Instructions burned: 2351 (million)
% 81.17/12.57 % (163570)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1802376813:i=134:gtgl=5:slsql=off:gtg=exists_sym_2973 on theBenchmark for (2973ds/134Mi)
% 81.17/12.57 % (163570)Instruction limit reached!
% 81.17/12.57 % (163570)------------------------------
% 81.17/12.57 % (163570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.17/12.57 % (163570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.17/12.57 % (163570)CaDiCaL version: 2.1.3
% 81.17/12.57 % (163570)Termination reason: Instruction limit
% 81.17/12.57 % (163570)Termination phase: Initialization
% 81.17/12.57 % (163570)Time elapsed: 0.059 s
% 81.17/12.57 % (163570)Peak memory usage: 96 MB
% 81.17/12.57 % (163570)Instructions burned: 134 (million)
% 81.17/12.57 % (163571)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=181510335:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/141Mi)
% 81.17/12.57 % (163573)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=661453093:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 81.17/12.57 % (163571)Instruction limit reached!
% 81.17/12.57 % (163571)------------------------------
% 81.17/12.57 % (163571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.17/12.57 % (163571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.17/12.57 % (163571)CaDiCaL version: 2.1.3
% 81.17/12.57 % (163571)Termination reason: Instruction limit
% 81.17/12.57 % (163571)Termination phase: Saturation
% 81.17/12.57 % (163571)Time elapsed: 0.083 s
% 81.17/12.57 % (163571)Peak memory usage: 101 MB
% 81.17/12.57 % (163571)Instructions burned: 141 (million)
% 81.17/12.57 % (163573)Refutation not found, incomplete strategy
% 81.17/12.57 % (163573)------------------------------
% 81.17/12.57 % (163573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.17/12.57 % (163573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.17/12.57 % (163573)CaDiCaL version: 2.1.3
% 81.17/12.57 % (163573)Termination reason: Refutation not found, incomplete strategy
% 81.17/12.57 % (163573)Time elapsed: 0.051 s
% 81.17/12.57 % (163573)Peak memory usage: 101 MB
% 81.17/12.57 % (163573)Instructions burned: 62 (million)
% 81.17/12.57 % (163576)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=646868445:i=6060:aac=none:ins=25_2968 on theBenchmark for (2968ds/6060Mi)
% 81.17/12.57 % (163573)------------------------------
% 81.17/12.57 % (163573)------------------------------
% 81.17/12.57 % (163578)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1264549989:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2966 on theBenchmark for (2966ds/150Mi)
% 81.17/12.57 % (163578)Instruction limit reached!
% 81.17/12.57 % (163578)------------------------------
% 81.17/12.57 % (163578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.17/12.57 % (163578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.17/12.57 % (163578)CaDiCaL version: 2.1.3
% 81.17/12.57 % (163578)Termination reason: Instruction limit
% 81.17/12.57 % (163578)Termination phase: Preprocessing 2
% 81.17/12.57 % (163578)Time elapsed: 0.115 s
% 81.17/12.57 % (163578)Peak memory usage: 102 MB
% 81.17/12.57 % (163578)Instructions burned: 150 (million)
% 111.02/17.47 % (163580)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1894681816:i=14155:bd=all_2963 on theBenchmark for (2963ds/14155Mi)
% 111.02/17.47 % (163559)Instruction limit reached!
% 111.02/17.47 % (163559)------------------------------
% 111.02/17.47 % (163559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163559)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163559)Termination reason: Instruction limit
% 111.02/17.47 % (163559)Termination phase: Saturation
% 111.02/17.47 % (163559)Time elapsed: 3.196 s
% 111.02/17.47 % (163559)Peak memory usage: 248 MB
% 111.02/17.47 % (163559)Instructions burned: 5202 (million)
% 111.02/17.47 % (163585)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2861187087:i=667:av=off:fsr=off_2951 on theBenchmark for (2951ds/667Mi)
% 111.02/17.47 % (163585)Instruction limit reached!
% 111.02/17.47 % (163585)------------------------------
% 111.02/17.47 % (163585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163585)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163585)Termination reason: Instruction limit
% 111.02/17.47 % (163585)Termination phase: Property scanning
% 111.02/17.47 % (163585)Time elapsed: 0.437 s
% 111.02/17.47 % (163585)Peak memory usage: 121 MB
% 111.02/17.47 % (163585)Instructions burned: 668 (million)
% 111.02/17.47 % (163587)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1045504216:s2a=on:i=185:s2at=1.8:fdi=4_2945 on theBenchmark for (2945ds/185Mi)
% 111.02/17.47 % (163587)Instruction limit reached!
% 111.02/17.47 % (163587)------------------------------
% 111.02/17.47 % (163587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163587)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163587)Termination reason: Instruction limit
% 111.02/17.47 % (163587)Termination phase: Preprocessing 2
% 111.02/17.47 % (163587)Time elapsed: 0.150 s
% 111.02/17.47 % (163587)Peak memory usage: 104 MB
% 111.02/17.47 % (163587)Instructions burned: 186 (million)
% 111.02/17.47 % (163589)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2572677406:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2942 on theBenchmark for (2942ds/193Mi)
% 111.02/17.47 % (163589)Instruction limit reached!
% 111.02/17.47 % (163589)------------------------------
% 111.02/17.47 % (163589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163589)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163589)Termination reason: Instruction limit
% 111.02/17.47 % (163589)Termination phase: Property scanning
% 111.02/17.47 % (163589)Time elapsed: 0.154 s
% 111.02/17.47 % (163589)Peak memory usage: 102 MB
% 111.02/17.47 % (163589)Instructions burned: 193 (million)
% 111.02/17.47 % (163591)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3847200016:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2938 on theBenchmark for (2938ds/4850Mi)
% 111.02/17.47 % (163576)Instruction limit reached!
% 111.02/17.47 % (163576)------------------------------
% 111.02/17.47 % (163576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163576)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163576)Termination reason: Instruction limit
% 111.02/17.47 % (163576)Termination phase: Saturation
% 111.02/17.47 % (163576)Time elapsed: 4.207 s
% 111.02/17.47 % (163576)Peak memory usage: 376 MB
% 111.02/17.47 % (163576)Instructions burned: 6060 (million)
% 111.02/17.47 % (163593)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2175952440:i=12111:sd=1:ss=included_2924 on theBenchmark for (2924ds/12111Mi)
% 111.02/17.47 % (163565)Instruction limit reached!
% 111.02/17.47 % (163565)------------------------------
% 111.02/17.47 % (163565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163565)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163565)Termination reason: Instruction limit
% 111.02/17.47 % (163565)Termination phase: Saturation
% 111.02/17.47 % (163565)Time elapsed: 6.319 s
% 111.02/17.47 % (163565)Peak memory usage: 236 MB
% 111.02/17.47 % (163565)Instructions burned: 13195 (million)
% 111.02/17.47 % (163591)Instruction limit reached!
% 111.02/17.47 % (163591)------------------------------
% 111.02/17.47 % (163591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163591)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163591)Termination reason: Instruction limit
% 111.02/17.47 % (163591)Termination phase: Saturation
% 111.02/17.47 % (163591)Time elapsed: 2.257 s
% 111.02/17.47 % (163591)Peak memory usage: 142 MB
% 111.02/17.47 % (163591)Instructions burned: 4850 (million)
% 111.02/17.47 % (163595)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2093917503:i=319:kws=precedence:fsr=off_2914 on theBenchmark for (2914ds/319Mi)
% 111.02/17.47 % (163596)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4004964909:i=2064:ep=RST_2914 on theBenchmark for (2914ds/2064Mi)
% 111.02/17.47 % (163595)Instruction limit reached!
% 111.02/17.47 % (163595)------------------------------
% 111.02/17.47 % (163595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163595)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163595)Termination reason: Instruction limit
% 111.02/17.47 % (163595)Termination phase: Preprocessing 3
% 111.02/17.47 % (163595)Time elapsed: 0.210 s
% 111.02/17.47 % (163595)Peak memory usage: 114 MB
% 111.02/17.47 % (163595)Instructions burned: 321 (million)
% 111.02/17.47 % (163599)dis-1011_128_sil=32000:random_seed=4047845269:i=3706:ep=RST:av=off_2911 on theBenchmark for (2911ds/3706Mi)
% 111.02/17.47 % (163596)Instruction limit reached!
% 111.02/17.47 % (163596)------------------------------
% 111.02/17.47 % (163596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163596)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163596)Termination reason: Instruction limit
% 111.02/17.47 % (163596)Termination phase: Saturation
% 111.02/17.47 % (163596)Time elapsed: 1.018 s
% 111.02/17.47 % (163596)Peak memory usage: 151 MB
% 111.02/17.47 % (163596)Instructions burned: 2066 (million)
% 111.02/17.47 % (163601)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2766333290:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2902 on theBenchmark for (2902ds/757Mi)
% 111.02/17.47 % (163601)Instruction limit reached!
% 111.02/17.47 % (163601)------------------------------
% 111.02/17.47 % (163601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163601)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163601)Termination reason: Instruction limit
% 111.02/17.47 % (163601)Termination phase: Saturation
% 111.02/17.47 % (163601)Time elapsed: 0.439 s
% 111.02/17.47 % (163601)Peak memory usage: 108 MB
% 111.02/17.47 % (163601)Instructions burned: 759 (million)
% 111.02/17.47 % (163599)Instruction limit reached!
% 111.02/17.47 % (163599)------------------------------
% 111.02/17.47 % (163599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163599)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163599)Termination reason: Instruction limit
% 111.02/17.47 % (163599)Termination phase: Saturation
% 111.02/17.47 % (163599)Time elapsed: 1.956 s
% 111.02/17.47 % (163599)Peak memory usage: 149 MB
% 111.02/17.47 % (163599)Instructions burned: 3708 (million)
% 111.02/17.47 % (163603)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2285937095:i=13913:ss=axioms:sgt=8_2891 on theBenchmark for (2891ds/13913Mi)
% 111.02/17.47 % (163604)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2128700996:i=9925:aac=none_2889 on theBenchmark for (2889ds/9925Mi)
% 111.02/17.47 % (163580)Instruction limit reached!
% 111.02/17.47 % (163580)------------------------------
% 111.02/17.47 % (163580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163580)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163580)Termination reason: Instruction limit
% 111.02/17.47 % (163580)Termination phase: Saturation
% 111.02/17.47 % (163580)Time elapsed: 8.088 s
% 111.02/17.47 % (163580)Peak memory usage: 412 MB
% 111.02/17.47 % (163580)Instructions burned: 14157 (million)
% 111.02/17.47 % (163607)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2392106627:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2880 on theBenchmark for (2880ds/2479Mi)
% 111.02/17.47 % (163607)Instruction limit reached!
% 111.02/17.47 % (163607)------------------------------
% 111.02/17.47 % (163607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163607)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163607)Termination reason: Instruction limit
% 111.02/17.47 % (163607)Termination phase: Saturation
% 111.02/17.47 % (163607)Time elapsed: 1.467 s
% 111.02/17.47 % (163607)Peak memory usage: 121 MB
% 111.02/17.47 % (163607)Instructions burned: 2479 (million)
% 111.02/17.47 % (163609)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=216214898:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2864 on theBenchmark for (2864ds/440Mi)
% 111.02/17.47 % (163609)Instruction limit reached!
% 111.02/17.47 % (163609)------------------------------
% 111.02/17.47 % (163609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163609)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163609)Termination reason: Instruction limit
% 111.02/17.47 % (163609)Termination phase: Naming
% 111.02/17.47 % (163609)Time elapsed: 0.239 s
% 111.02/17.47 % (163609)Peak memory usage: 109 MB
% 111.02/17.47 % (163609)Instructions burned: 440 (million)
% 111.02/17.47 % (163611)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3260718425:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2859 on theBenchmark for (2859ds/11145Mi)
% 111.02/17.47 % (163593)Instruction limit reached!
% 111.02/17.47 % (163593)------------------------------
% 111.02/17.47 % (163593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163593)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163593)Termination reason: Instruction limit
% 111.02/17.47 % (163593)Termination phase: Saturation
% 111.02/17.47 % (163593)Time elapsed: 6.880 s
% 111.02/17.47 % (163593)Peak memory usage: 249 MB
% 111.02/17.47 % (163593)Instructions burned: 12114 (million)
% 111.02/17.47 % (163613)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=266107167:cts=off:i=3034:av=off:er=known:fsd=on_2854 on theBenchmark for (2854ds/3034Mi)
% 111.02/17.47 % (163611)First to succeed.
% 111.02/17.47 % (163611)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-163519"
% 111.02/17.47 % (163613)Instruction limit reached!
% 111.02/17.47 % (163613)------------------------------
% 111.02/17.47 % (163613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.02/17.47 % (163613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.02/17.47 % (163613)CaDiCaL version: 2.1.3
% 111.02/17.47 % (163613)Termination reason: Instruction limit
% 111.02/17.47 % (163613)Termination phase: Saturation
% 111.02/17.47 % (163613)Time elapsed: 1.992 s
% 111.02/17.47 % (163613)Peak memory usage: 269 MB
% 111.02/17.47 % (163613)Instructions burned: 3037 (million)
% 111.02/17.47 % (163611)Refutation found. Thanks to Tanya!
% 111.02/17.47 % SZS status Theorem for theBenchmark
% 111.02/17.47 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/17.70 % (163611)------------------------------
% 0.17/17.70 % (163611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/17.70 % (163611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/17.70 % (163611)CaDiCaL version: 2.1.3
% 0.17/17.70 % (163611)Termination reason: Refutation
% 0.17/17.70 % (163611)Time elapsed: 2.319 s
% 0.17/17.70 % (163611)Peak memory usage: 170 MB
% 0.17/17.70 % (163611)Instructions burned: 3606 (million)
% 0.17/17.70 % (163611)------------------------------
% 0.17/17.70 % (163611)------------------------------
% 0.17/17.70 % (163519)Success in time 16.813 s
% 0.17/17.70 % Vampire exiting
%------------------------------------------------------------------------------