%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG218+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:29:49 AM UTC 2026
% Result : Theorem 6.50s 3.95s
% Output : Refutation 6.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 25
% Syntax : Number of formulae : 211 ( 66 unt; 6 def)
% Number of atoms : 1109 ( 128 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 1552 ( 654 ~; 691 |; 173 &)
% ( 9 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 10 con; 0-3 aty)
% Number of variables : 212 ( 201 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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(f2,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)],[f1]) ).
fof(f8,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f9,axiom,
! [X0,X1] :
( X1 = k1_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tarski) ).
fof(f10,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(f12,axiom,
! [X0] :
( l2_struct_0(X0)
=> m1_subset_1(k1_rlvect_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_rlvect_1) ).
fof(f21,axiom,
! [X0] :
( l1_rlvect_1(X0)
=> l2_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_rlvect_1) ).
fof(f24,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(f25,axiom,
! [X0] :
( l2_struct_0(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_struct_0) ).
fof(f26,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(f27,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(f48,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f61,axiom,
! [X0] :
? [X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(f68,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(f71,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(f72,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f73,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f74,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f75,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(f78,axiom,
! [X0] :
( v1_xboole_0(X0)
=> X0 = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f87,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,[],[f2]) ).
fof(f88,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,[],[f87]) ).
fof(f96,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f99,plain,
! [X0] :
( m1_subset_1(k1_rlvect_1(X0),u1_struct_0(X0))
| ~ l2_struct_0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f107,plain,
! [X0] :
( l2_struct_0(X0)
| ~ l1_rlvect_1(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f109,plain,
! [X0] :
( ! [X1] :
( l1_rlvect_1(X1)
| ~ l1_vectsp_2(X1,X0) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f110,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_struct_0(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f111,plain,
! [X0] :
( ( l1_vectsp_1(X0)
& l2_struct_0(X0) )
| ~ l2_vectsp_1(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f112,plain,
! [X0] :
( ( l1_rlvect_1(X0)
& l2_vectsp_1(X0) )
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f123,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f124,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f123]) ).
fof(f144,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,[],[f68]) ).
fof(f145,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,[],[f144]) ).
fof(f146,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,[],[f71]) ).
fof(f147,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,[],[f146]) ).
fof(f148,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f72]) ).
fof(f149,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f73]) ).
fof(f150,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f149]) ).
fof(f151,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,[],[f75]) ).
fof(f152,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,[],[f151]) ).
fof(f156,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f78]) ).
fof(f159,plain,
( k1_rmod_5(sK0,sK1,sK2) = k1_rmod_2(sK0,sK1)
& k1_xboole_0 != sK2
& sK2 != k7_rlvect_2(sK1,k1_rlvect_1(sK1))
& m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
& ~ v3_struct_0(sK1)
& v3_rlvect_1(sK1)
& v4_rlvect_1(sK1)
& v5_rlvect_1(sK1)
& v6_rlvect_1(sK1)
& v5_vectsp_2(sK1,sK0)
& l1_vectsp_2(sK1,sK0)
& ~ v3_struct_0(sK0)
& v3_rlvect_1(sK0)
& v4_rlvect_1(sK0)
& v5_rlvect_1(sK0)
& v6_rlvect_1(sK0)
& v4_group_1(sK0)
& v7_group_1(sK0)
& v6_vectsp_1(sK0)
& v7_vectsp_1(sK0)
& v8_vectsp_1(sK0)
& ~ v10_vectsp_1(sK0)
& v2_vectsp_2(sK0)
& l3_vectsp_1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f88]) ).
fof(f160,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f161,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f160]) ).
fof(f162,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,[],[f9]) ).
fof(f163,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,[],[f162]) ).
fof(f164,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ( ( sK3(X0,X1) != X0
| ~ r2_hidden(sK3(X0,X1),X1) )
& ( sK3(X0,X1) = X0
| r2_hidden(sK3(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,[sK3]),skolemize(X2,sK3(X0,X1))],[f163]) ).
fof(f165,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,[],[f96]) ).
fof(f166,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,[],[f165]) ).
fof(f167,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK4(X0,X1),X1)
& r2_hidden(sK4(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f166]) ).
fof(f186,plain,
! [X0] :
( m1_subset_1(sK23(X0),k1_zfmisc_1(X0))
& v1_xboole_0(sK23(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(X1,sK23(X0))],[f61]) ).
fof(f194,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f74]) ).
fof(f195,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,[],[f152]) ).
fof(f196,plain,
l3_vectsp_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f197,plain,
v2_vectsp_2(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f198,plain,
~ v10_vectsp_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f199,plain,
v8_vectsp_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f200,plain,
v7_vectsp_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f201,plain,
v6_vectsp_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f202,plain,
v7_group_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f203,plain,
v4_group_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f204,plain,
v6_rlvect_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f205,plain,
v5_rlvect_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f206,plain,
v4_rlvect_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f207,plain,
v3_rlvect_1(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f208,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f209,plain,
l1_vectsp_2(sK1,sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f210,plain,
v5_vectsp_2(sK1,sK0),
inference(cnf_transformation,[],[f159]) ).
fof(f211,plain,
v6_rlvect_1(sK1),
inference(cnf_transformation,[],[f159]) ).
fof(f212,plain,
v5_rlvect_1(sK1),
inference(cnf_transformation,[],[f159]) ).
fof(f213,plain,
v4_rlvect_1(sK1),
inference(cnf_transformation,[],[f159]) ).
fof(f214,plain,
v3_rlvect_1(sK1),
inference(cnf_transformation,[],[f159]) ).
fof(f215,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f159]) ).
fof(f216,plain,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))),
inference(cnf_transformation,[],[f159]) ).
fof(f217,plain,
sK2 != k7_rlvect_2(sK1,k1_rlvect_1(sK1)),
inference(cnf_transformation,[],[f159]) ).
fof(f218,plain,
k1_xboole_0 != sK2,
inference(cnf_transformation,[],[f159]) ).
fof(f219,plain,
k1_rmod_5(sK0,sK1,sK2) = k1_rmod_2(sK0,sK1),
inference(cnf_transformation,[],[f159]) ).
fof(f230,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f161]) ).
fof(f231,plain,
! [X3,X0,X1] :
( X0 = X3
| ~ r2_hidden(X3,X1)
| k1_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f164]) ).
fof(f232,plain,
! [X3,X0,X1] :
( r2_hidden(X3,X1)
| X0 != X3
| k1_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f164]) ).
fof(f236,plain,
! [X0,X1] :
( r2_hidden(sK4(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f237,plain,
! [X0,X1] :
( ~ r2_hidden(sK4(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f240,plain,
! [X0] :
( m1_subset_1(k1_rlvect_1(X0),u1_struct_0(X0))
| ~ l2_struct_0(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f247,plain,
! [X0] :
( ~ l1_rlvect_1(X0)
| l2_struct_0(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f249,plain,
! [X0,X1] :
( ~ l1_vectsp_2(X1,X0)
| l1_rlvect_1(X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f109]) ).
fof(f250,plain,
! [X0] :
( ~ l2_struct_0(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f251,plain,
! [X0] :
( ~ l2_vectsp_1(X0)
| l2_struct_0(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f253,plain,
! [X0] :
( ~ l3_vectsp_1(X0)
| l2_vectsp_1(X0) ),
inference(cnf_transformation,[],[f112]) ).
fof(f282,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f322,plain,
! [X0] : v1_xboole_0(sK23(X0)),
inference(cnf_transformation,[],[f186]) ).
fof(f323,plain,
! [X0] : m1_subset_1(sK23(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f186]) ).
fof(f335,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| k7_rlvect_2(X0,X1) = k1_tarski(X1) ),
inference(cnf_transformation,[],[f145]) ).
fof(f339,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,[],[f147]) ).
fof(f340,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f148]) ).
fof(f341,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f150]) ).
fof(f342,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f194]) ).
fof(f344,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,[],[f195]) ).
fof(f348,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f156]) ).
fof(f353,plain,
! [X3,X1] :
( r2_hidden(X3,X1)
| k1_tarski(X3) != X1 ),
inference(equality_resolution,[],[f232]) ).
fof(f354,plain,
! [X3] : r2_hidden(X3,k1_tarski(X3)),
inference(equality_resolution,[],[f353]) ).
fof(f355,plain,
! [X3,X0] :
( ~ r2_hidden(X3,k1_tarski(X0))
| X0 = X3 ),
inference(equality_resolution,[],[f231]) ).
fof(f357,definition,
sF30 = k1_rmod_5(sK0,sK1,sK2),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f358,plain,
k1_rmod_5(sK0,sK1,sK2) = sF30,
inference(reorient_equations,[],[f357]) ).
fof(f359,definition,
sF31 = k1_rmod_2(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f360,plain,
k1_rmod_2(sK0,sK1) = sF31,
inference(reorient_equations,[],[f359]) ).
fof(f361,plain,
sF30 = sF31,
inference(definition_folding,[],[f219,f360,f358]) ).
fof(f362,definition,
sF32 = k1_rlvect_1(sK1),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f363,plain,
k1_rlvect_1(sK1) = sF32,
inference(reorient_equations,[],[f362]) ).
fof(f364,definition,
sF33 = k7_rlvect_2(sK1,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f365,plain,
k7_rlvect_2(sK1,sF32) = sF33,
inference(reorient_equations,[],[f364]) ).
fof(f366,plain,
sK2 != sF33,
inference(definition_folding,[],[f217,f365,f363]) ).
fof(f367,definition,
sF34 = u1_struct_0(sK1),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f368,plain,
u1_struct_0(sK1) = sF34,
inference(reorient_equations,[],[f367]) ).
fof(f369,definition,
sF35 = k1_zfmisc_1(sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f370,plain,
k1_zfmisc_1(sF34) = sF35,
inference(reorient_equations,[],[f369]) ).
fof(f371,plain,
m1_subset_1(sK2,sF35),
inference(definition_folding,[],[f216,f370,f368]) ).
fof(f372,plain,
k1_rmod_2(sK0,sK1) = sF30,
inference(forward_demodulation,[],[f360,f361]) ).
fof(f383,plain,
l2_vectsp_1(sK0),
inference(resolution,[],[f253,f196]) ).
fof(f386,plain,
l2_struct_0(sK0),
inference(resolution,[],[f383,f251]) ).
fof(f391,plain,
l1_struct_0(sK0),
inference(resolution,[],[f386,f250]) ).
fof(f401,plain,
! [X0] : k1_xboole_0 = sK23(X0),
inference(resolution,[],[f348,f322]) ).
fof(f414,plain,
( m1_subset_1(k1_rlvect_1(sK1),sF34)
| ~ l2_struct_0(sK1) ),
inference(superposition,[],[f240,f368]) ).
fof(f415,plain,
( m1_subset_1(sF32,sF34)
| ~ l2_struct_0(sK1) ),
inference(forward_demodulation,[],[f414,f363]) ).
fof(f417,plain,
( l1_rlvect_1(sK1)
| ~ l1_struct_0(sK0) ),
inference(resolution,[],[f249,f209]) ).
fof(f424,plain,
l1_rlvect_1(sK1),
inference(forward_subsumption_resolution,[],[f417,f391]) ).
fof(f425,plain,
l2_struct_0(sK1),
inference(resolution,[],[f424,f247]) ).
fof(f428,plain,
l1_struct_0(sK1),
inference(resolution,[],[f425,f250]) ).
fof(f429,plain,
( ~ v1_xboole_0(sF34)
| v3_struct_0(sK1)
| ~ l1_struct_0(sK1) ),
inference(superposition,[],[f282,f368]) ).
fof(f430,plain,
( ~ v1_xboole_0(sF34)
| ~ l1_struct_0(sK1) ),
inference(forward_subsumption_resolution,[],[f429,f215]) ).
fof(f431,plain,
~ v1_xboole_0(sF34),
inference(forward_subsumption_resolution,[],[f430,f428]) ).
fof(f436,plain,
! [X0] : r1_tarski(sK23(X0),X0),
inference(resolution,[],[f342,f323]) ).
fof(f438,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(forward_demodulation,[],[f436,f401]) ).
fof(f474,plain,
( r2_hidden(sF32,sF34)
| v1_xboole_0(sF34)
| ~ l2_struct_0(sK1) ),
inference(resolution,[],[f341,f415]) ).
fof(f475,plain,
( r2_hidden(sF32,sF34)
| ~ l2_struct_0(sK1) ),
inference(forward_subsumption_resolution,[],[f474,f431]) ).
fof(f485,plain,
r2_hidden(sF32,sF34),
inference(forward_subsumption_resolution,[],[f475,f425]) ).
fof(f496,plain,
m1_subset_1(sF32,sF34),
inference(resolution,[],[f485,f340]) ).
fof(f578,plain,
! [X0] :
( ~ m1_subset_1(X0,sF34)
| v3_struct_0(sK1)
| ~ l1_struct_0(sK1)
| k1_tarski(X0) = k7_rlvect_2(sK1,X0) ),
inference(superposition,[],[f335,f368]) ).
fof(f579,plain,
! [X0] :
( ~ m1_subset_1(X0,sF34)
| ~ l1_struct_0(sK1)
| k1_tarski(X0) = k7_rlvect_2(sK1,X0) ),
inference(forward_subsumption_resolution,[],[f578,f215]) ).
fof(f582,plain,
! [X0] :
( ~ m1_subset_1(X0,sF34)
| k1_tarski(X0) = k7_rlvect_2(sK1,X0) ),
inference(forward_subsumption_resolution,[],[f579,f428]) ).
fof(f626,plain,
k7_rlvect_2(sK1,sF32) = k1_tarski(sF32),
inference(resolution,[],[f582,f496]) ).
fof(f629,plain,
sF33 = k1_tarski(sF32),
inference(forward_demodulation,[],[f626,f365]) ).
fof(f631,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| sF32 = X0 ),
inference(superposition,[],[f355,f629]) ).
fof(f634,plain,
r2_hidden(sF32,sF33),
inference(superposition,[],[f354,f629]) ).
fof(f643,plain,
! [X0] :
( r1_tarski(sF33,X0)
| sF32 = sK4(sF33,X0) ),
inference(resolution,[],[f631,f236]) ).
fof(f955,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(superposition,[],[f344,f372]) ).
fof(f957,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f955,f215]) ).
fof(f958,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f957,f214]) ).
fof(f959,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f958,f213]) ).
fof(f960,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f959,f212]) ).
fof(f961,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f960,f211]) ).
fof(f962,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f961,f210]) ).
fof(f963,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f962,f209]) ).
fof(f964,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f963,f208]) ).
fof(f965,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f964,f207]) ).
fof(f966,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f965,f206]) ).
fof(f967,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f966,f205]) ).
fof(f968,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v4_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f967,f204]) ).
fof(f969,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f968,f203]) ).
fof(f970,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f969,f201]) ).
fof(f971,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ v8_vectsp_1(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f970,f200]) ).
fof(f972,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f971,f199]) ).
fof(f973,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| k1_rlvect_1(sK1) = X0 ),
inference(forward_subsumption_resolution,[],[f972,f196]) ).
fof(f974,plain,
! [X0] :
( ~ r1_rlvect_1(sF30,X0)
| sF32 = X0 ),
inference(forward_demodulation,[],[f973,f363]) ).
fof(f1011,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(superposition,[],[f339,f358]) ).
fof(f1012,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v3_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1011,f215]) ).
fof(f1013,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v4_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1012,f214]) ).
fof(f1014,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v5_rlvect_1(sK1)
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1013,f213]) ).
fof(f1015,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v6_rlvect_1(sK1)
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1014,f212]) ).
fof(f1016,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v5_vectsp_2(sK1,sK0)
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1015,f211]) ).
fof(f1017,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1016,f210]) ).
fof(f1018,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK0)
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1017,f209]) ).
fof(f1019,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v3_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1018,f208]) ).
fof(f1020,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v4_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1019,f207]) ).
fof(f1021,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v5_rlvect_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1020,f206]) ).
fof(f1022,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v6_rlvect_1(sK0)
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1021,f205]) ).
fof(f1023,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v4_group_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1022,f204]) ).
fof(f1024,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v7_group_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1023,f203]) ).
fof(f1025,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v6_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1024,f202]) ).
fof(f1026,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v7_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1025,f201]) ).
fof(f1027,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v8_vectsp_1(sK0)
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1026,f200]) ).
fof(f1028,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v10_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1027,f199]) ).
fof(f1029,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v2_vectsp_2(sK0)
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1028,f198]) ).
fof(f1030,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_vectsp_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1029,f197]) ).
fof(f1031,plain,
! [X0] :
( r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(forward_subsumption_resolution,[],[f1030,f196]) ).
fof(f1032,plain,
! [X0] :
( ~ m1_subset_1(sK2,k1_zfmisc_1(sF34))
| r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2) ),
inference(forward_demodulation,[],[f1031,f368]) ).
fof(f1033,plain,
! [X0] :
( ~ m1_subset_1(sK2,sF35)
| r1_rlvect_1(sF30,X0)
| ~ r2_hidden(X0,sK2) ),
inference(forward_demodulation,[],[f1032,f370]) ).
fof(f1034,plain,
! [X0] :
( ~ r2_hidden(X0,sK2)
| r1_rlvect_1(sF30,X0) ),
inference(forward_subsumption_resolution,[],[f1033,f371]) ).
fof(f1036,plain,
! [X0] :
( r1_rlvect_1(sF30,sK4(sK2,X0))
| r1_tarski(sK2,X0) ),
inference(resolution,[],[f1034,f236]) ).
fof(f1040,plain,
! [X0] :
( r1_tarski(sK2,X0)
| sF32 = sK4(sK2,X0) ),
inference(resolution,[],[f1036,f974]) ).
fof(f1043,plain,
! [X0] :
( ~ r1_tarski(X0,sK2)
| sF32 = sK4(sK2,X0)
| sK2 = X0 ),
inference(resolution,[],[f1040,f230]) ).
fof(f1065,plain,
( sF32 = sK4(sK2,k1_xboole_0)
| k1_xboole_0 = sK2 ),
inference(resolution,[],[f1043,f438]) ).
fof(f1071,plain,
( sF32 = sK4(sK2,sF33)
| sK2 = sF33
| sF32 = sK4(sF33,sK2) ),
inference(resolution,[],[f1043,f643]) ).
fof(f1074,plain,
( sF32 = sK4(sF33,sK2)
| sF32 = sK4(sK2,sF33) ),
inference(forward_subsumption_resolution,[],[f1071,f366]) ).
fof(f1075,plain,
sF32 = sK4(sK2,k1_xboole_0),
inference(forward_subsumption_resolution,[],[f1065,f218]) ).
fof(f1173,plain,
( r1_tarski(sK2,k1_xboole_0)
| r2_hidden(sF32,sK2) ),
inference(superposition,[],[f236,f1075]) ).
fof(f1359,plain,
( r2_hidden(sF32,sK2)
| ~ r1_tarski(k1_xboole_0,sK2)
| k1_xboole_0 = sK2 ),
inference(resolution,[],[f1173,f230]) ).
fof(f1360,plain,
( r2_hidden(sF32,sK2)
| k1_xboole_0 = sK2 ),
inference(forward_subsumption_resolution,[],[f1359,f438]) ).
fof(f1362,plain,
r2_hidden(sF32,sK2),
inference(forward_subsumption_resolution,[],[f1360,f218]) ).
fof(f3368,plain,
( ~ r2_hidden(sF32,sK2)
| r1_tarski(sF33,sK2)
| sF32 = sK4(sK2,sF33) ),
inference(superposition,[],[f237,f1074]) ).
fof(f3370,plain,
( r1_tarski(sF33,sK2)
| sF32 = sK4(sK2,sF33) ),
inference(forward_subsumption_resolution,[],[f3368,f1362]) ).
fof(f3375,plain,
( sF32 = sK4(sK2,sF33)
| sF32 = sK4(sK2,sF33)
| sK2 = sF33 ),
inference(resolution,[],[f3370,f1043]) ).
fof(f3381,plain,
( sF32 = sK4(sK2,sF33)
| sK2 = sF33 ),
inference(duplicate_literal_removal,[],[f3375]) ).
fof(f3383,plain,
sF32 = sK4(sK2,sF33),
inference(forward_subsumption_resolution,[],[f3381,f366]) ).
fof(f3396,plain,
( ~ r2_hidden(sF32,sF33)
| r1_tarski(sK2,sF33) ),
inference(superposition,[],[f237,f3383]) ).
fof(f3398,plain,
r1_tarski(sK2,sF33),
inference(forward_subsumption_resolution,[],[f3396,f634]) ).
fof(f3473,plain,
( ~ r1_tarski(sF33,sK2)
| sK2 = sF33 ),
inference(resolution,[],[f3398,f230]) ).
fof(f3474,plain,
~ r1_tarski(sF33,sK2),
inference(forward_subsumption_resolution,[],[f3473,f366]) ).
fof(f3489,plain,
sF32 = sK4(sF33,sK2),
inference(resolution,[],[f3474,f643]) ).
fof(f3499,plain,
( ~ r2_hidden(sF32,sK2)
| r1_tarski(sF33,sK2) ),
inference(superposition,[],[f237,f3489]) ).
fof(f3501,plain,
r1_tarski(sF33,sK2),
inference(forward_subsumption_resolution,[],[f3499,f1362]) ).
fof(f3502,plain,
$false,
inference(forward_subsumption_resolution,[],[f3501,f3474]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG218+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:46:16 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.37/2.41 % (3699197)Will run a generic schedule for satisfiability detection.
% 15.37/2.41 % (3699205)dis+10_1_sil=32000:sp=arity:random_seed=3618217850:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.37/2.41 % (3699203)% WARNING: option uhcvi not known.
% 15.37/2.41 % (3699203)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1967424775:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.37/2.41 % (3699202)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1817801597_2999 on theBenchmark for (2999ds/0Mi)
% 15.37/2.41 % (3699207)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3974820845:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.37/2.41 % (3699206)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1176059070:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.37/2.41 % (3699208)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1970409164:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.37/2.41 % (3699204)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2533685813:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.37/2.41 % TRYING [1]
% 15.37/2.41 % TRYING [2]
% 15.37/2.41 % TRYING [3]
% 15.37/2.41 % (3699205)Instruction limit reached!
% 15.37/2.41 % (3699205)------------------------------
% 15.37/2.41 % (3699205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.41 % (3699205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.41 % (3699205)CaDiCaL version: 2.1.3
% 15.37/2.41 % (3699205)Termination reason: Instruction limit
% 15.37/2.41 % (3699205)Termination phase: Saturation
% 15.37/2.41 % (3699205)Time elapsed: 0.035 s
% 15.37/2.41 % (3699205)Peak memory usage: 13 MB
% 15.37/2.41 % (3699205)Instructions burned: 105 (million)
% 15.37/2.41 % (3699216)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1266117051:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.37/2.41 % TRYING [1]
% 15.37/2.41 % TRYING [2]
% 15.37/2.41 % TRYING [3]
% 15.37/2.41 % TRYING [4]
% 15.37/2.41 % (3699206)Instruction limit reached!
% 15.37/2.41 % (3699206)------------------------------
% 15.37/2.41 % (3699206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.41 % (3699206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.41 % (3699206)CaDiCaL version: 2.1.3
% 15.37/2.41 % (3699206)Termination reason: Instruction limit
% 15.37/2.41 % (3699206)Termination phase: Saturation
% 15.37/2.41 % (3699206)Time elapsed: 0.068 s
% 15.37/2.41 % (3699206)Peak memory usage: 13 MB
% 15.37/2.41 % (3699206)Instructions burned: 118 (million)
% 15.37/2.41 % (3699207)Instruction limit reached!
% 15.37/2.41 % (3699207)------------------------------
% 15.37/2.41 % (3699207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.41 % (3699207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.41 % (3699207)CaDiCaL version: 2.1.3
% 15.37/2.41 % (3699207)Termination reason: Instruction limit
% 15.37/2.41 % (3699207)Termination phase: Saturation
% 15.37/2.41 % (3699207)Time elapsed: 0.075 s
% 15.37/2.41 % (3699207)Peak memory usage: 13 MB
% 15.37/2.41 % (3699207)Instructions burned: 131 (million)
% 15.37/2.41 % (3699218)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1411481029:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.37/2.41 % (3699208)Instruction limit reached!
% 15.37/2.41 % (3699208)------------------------------
% 15.37/2.41 % (3699208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.41 % (3699208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.41 % (3699208)CaDiCaL version: 2.1.3
% 15.37/2.41 % (3699208)Termination reason: Instruction limit
% 15.37/2.41 % (3699208)Termination phase: Saturation
% 15.37/2.41 % (3699208)Time elapsed: 0.090 s
% 15.37/2.41 % (3699208)Peak memory usage: 15 MB
% 15.37/2.41 % (3699208)Instructions burned: 160 (million)
% 15.37/2.41 % (3699219)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1390994144:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.37/2.41 % (3699221)ott-21_1_sil=16000:fs=off:random_seed=61012661:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.37/2.41 % (3699218)Instruction limit reached!
% 15.37/2.41 % (3699218)------------------------------
% 15.37/2.41 % (3699218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.41 % (3699218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699218)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699218)Termination reason: Instruction limit
% 6.50/3.95 % (3699218)Termination phase: Saturation
% 6.50/3.95 % (3699218)Time elapsed: 0.071 s
% 6.50/3.95 % (3699218)Peak memory usage: 14 MB
% 6.50/3.95 % (3699218)Instructions burned: 133 (million)
% 6.50/3.95 % (3699216)Instruction limit reached!
% 6.50/3.95 % (3699216)------------------------------
% 6.50/3.95 % (3699216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699216)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699216)Termination reason: Instruction limit
% 6.50/3.95 % (3699216)Termination phase: Finite model building constraint generation
% 6.50/3.95 % (3699216)Time elapsed: 0.125 s
% 6.50/3.95 % (3699216)Peak memory usage: 25 MB
% 6.50/3.95 % (3699216)Instructions burned: 715 (million)
% 6.50/3.95 % (3699225)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2339340591:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.50/3.95 % TRYING [1]
% 6.50/3.95 % (3699224)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3338893734:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.50/3.95 % TRYING [2]
% 6.50/3.95 % TRYING [3]
% 6.50/3.95 % TRYING [5]
% 6.50/3.95 % (3699221)Instruction limit reached!
% 6.50/3.95 % (3699221)------------------------------
% 6.50/3.95 % (3699221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699221)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699221)Termination reason: Instruction limit
% 6.50/3.95 % (3699221)Termination phase: Saturation
% 6.50/3.95 % (3699221)Time elapsed: 0.094 s
% 6.50/3.95 % (3699221)Peak memory usage: 13 MB
% 6.50/3.95 % (3699221)Instructions burned: 181 (million)
% 6.50/3.95 % (3699228)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1407852845:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 6.50/3.95 % TRYING [4]
% 6.50/3.95 % (3699225)Instruction limit reached!
% 6.50/3.95 % (3699225)------------------------------
% 6.50/3.95 % (3699225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699225)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699225)Termination reason: Instruction limit
% 6.50/3.95 % (3699225)Termination phase: Finite model building SAT solving
% 6.50/3.95 % (3699225)Time elapsed: 0.186 s
% 6.50/3.95 % (3699225)Peak memory usage: 31 MB
% 6.50/3.95 % (3699225)Instructions burned: 868 (million)
% 6.50/3.95 % (3699230)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=88584091:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 6.50/3.95 % (3699224)Instruction limit reached!
% 6.50/3.95 % (3699224)------------------------------
% 6.50/3.95 % (3699224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699224)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699224)Termination reason: Instruction limit
% 6.50/3.95 % (3699224)Termination phase: Saturation
% 6.50/3.95 % (3699224)Time elapsed: 0.323 s
% 6.50/3.95 % (3699224)Peak memory usage: 15 MB
% 6.50/3.95 % (3699224)Instructions burned: 478 (million)
% 6.50/3.95 % (3699219)Instruction limit reached!
% 6.50/3.95 % (3699219)------------------------------
% 6.50/3.95 % (3699219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699219)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699219)Termination reason: Instruction limit
% 6.50/3.95 % (3699219)Termination phase: Saturation
% 6.50/3.95 % (3699219)Time elapsed: 0.426 s
% 6.50/3.95 % (3699219)Peak memory usage: 19 MB
% 6.50/3.95 % (3699219)Instructions burned: 685 (million)
% 6.50/3.95 % (3699232)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1821163108:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 6.50/3.95 % (3699233)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1292951788:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 6.50/3.95 % (3699230)Instruction limit reached!
% 6.50/3.95 % (3699230)------------------------------
% 6.50/3.95 % (3699230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699230)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699230)Termination reason: Instruction limit
% 6.50/3.95 % (3699230)Termination phase: Finite model building constraint generation
% 6.50/3.95 % (3699230)Time elapsed: 0.231 s
% 6.50/3.95 % (3699230)Peak memory usage: 106 MB
% 6.50/3.95 % (3699230)Instructions burned: 891 (million)
% 6.50/3.95 % (3699236)fmb+10_1_sil=64000:random_seed=3170449128:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 6.50/3.95 % TRYING [1]
% 6.50/3.95 % TRYING [2]
% 6.50/3.95 % TRYING [3]
% 6.50/3.95 % TRYING [6]
% 6.50/3.95 % (3699228)Instruction limit reached!
% 6.50/3.95 % (3699228)------------------------------
% 6.50/3.95 % (3699228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699228)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699228)Termination reason: Instruction limit
% 6.50/3.95 % (3699228)Termination phase: Saturation
% 6.50/3.95 % (3699228)Time elapsed: 0.613 s
% 6.50/3.95 % (3699228)Peak memory usage: 21 MB
% 6.50/3.95 % (3699228)Instructions burned: 1179 (million)
% 6.50/3.95 % (3699238)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1958706687:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 6.50/3.95 % TRYING [20]
% 6.50/3.95 % (3699232)Instruction limit reached!
% 6.50/3.95 % (3699232)------------------------------
% 6.50/3.95 % (3699232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699232)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699232)Termination reason: Instruction limit
% 6.50/3.95 % (3699232)Termination phase: Saturation
% 6.50/3.95 % (3699232)Time elapsed: 0.440 s
% 6.50/3.95 % (3699232)Peak memory usage: 20 MB
% 6.50/3.95 % (3699232)Instructions burned: 693 (million)
% 6.50/3.95 % (3699240)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=312766264:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 6.50/3.95 % TRYING [8]
% 6.50/3.95 % (3699233)Instruction limit reached!
% 6.50/3.95 % (3699233)------------------------------
% 6.50/3.95 % (3699233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699233)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699233)Termination reason: Instruction limit
% 6.50/3.95 % (3699233)Termination phase: Saturation
% 6.50/3.95 % (3699233)Time elapsed: 0.505 s
% 6.50/3.95 % (3699233)Peak memory usage: 20 MB
% 6.50/3.95 % (3699233)Instructions burned: 880 (million)
% 6.50/3.95 % (3699242)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1949920357:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 6.50/3.95 % (3699240)Instruction limit reached!
% 6.50/3.95 % (3699240)------------------------------
% 6.50/3.95 % (3699240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699240)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699240)Termination reason: Instruction limit
% 6.50/3.95 % (3699240)Termination phase: Finite model building constraint generation
% 6.50/3.95 % (3699240)Time elapsed: 0.298 s
% 6.50/3.95 % (3699240)Peak memory usage: 59 MB
% 6.50/3.95 % (3699240)Instructions burned: 920 (million)
% 6.50/3.95 % (3699244)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2094827505:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 6.50/3.95 % (3699244)Instruction limit reached!
% 6.50/3.95 % (3699244)------------------------------
% 6.50/3.95 % (3699244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699244)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699244)Termination reason: Instruction limit
% 6.50/3.95 % (3699244)Termination phase: Saturation
% 6.50/3.95 % (3699244)Time elapsed: 0.799 s
% 6.50/3.95 % (3699244)Peak memory usage: 20 MB
% 6.50/3.95 % (3699244)Instructions burned: 1473 (million)
% 6.50/3.95 % (3699246)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3937861662:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 6.50/3.95 % (3699246)Cannot represent all propositional literals internally
% 6.50/3.95 % (3699246)Refutation not found, incomplete strategy
% 6.50/3.95 % (3699246)------------------------------
% 6.50/3.95 % (3699246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699246)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699246)Termination reason: Refutation not found, incomplete strategy
% 6.50/3.95 % (3699246)Time elapsed: 0.017 s
% 6.50/3.95 % (3699246)Peak memory usage: 11 MB
% 6.50/3.95 % (3699246)Instructions burned: 35 (million)
% 6.50/3.95 % (3699246)------------------------------
% 6.50/3.95 % (3699246)------------------------------
% 6.50/3.95 % (3699248)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3672600649:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 6.50/3.95 % TRYING [16]
% 6.50/3.95 % TRYING [7]
% 6.50/3.95 % (3699248)Instruction limit reached!
% 6.50/3.95 % (3699248)------------------------------
% 6.50/3.95 % (3699248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699248)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699248)Termination reason: Instruction limit
% 6.50/3.95 % (3699248)Termination phase: Finite model building constraint generation
% 6.50/3.95 % (3699248)Time elapsed: 0.766 s
% 6.50/3.95 % (3699248)Peak memory usage: 133 MB
% 6.50/3.95 % (3699248)Instructions burned: 2175 (million)
% 6.50/3.95 % (3699250)ott-2_1_sil=16000:newcnf=on:random_seed=1988681136:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 6.50/3.95 % (3699250)Instruction limit reached!
% 6.50/3.95 % (3699250)------------------------------
% 6.50/3.95 % (3699250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699250)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699250)Termination reason: Instruction limit
% 6.50/3.95 % (3699250)Termination phase: Saturation
% 6.50/3.95 % (3699250)Time elapsed: 0.533 s
% 6.50/3.95 % (3699250)Peak memory usage: 17 MB
% 6.50/3.95 % (3699250)Instructions burned: 870 (million)
% 6.50/3.95 % (3699252)ott+10_1_sil=32000:tgt=ground:random_seed=3766822573:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 6.50/3.95 % (3699252) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3699197-3699252"...
% 6.50/3.95 % (3699252)...printing done.
% 6.50/3.95 % (3699252)Refutation found. Thanks to Tanya!
% 6.50/3.95 % SZS status Theorem for theBenchmark
% 6.50/3.95 % SZS output start Proof for theBenchmark
% See solution above
% 6.50/3.95 % (3699252)------------------------------
% 6.50/3.95 % (3699252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/3.95 % (3699252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/3.95 % (3699252)CaDiCaL version: 2.1.3
% 6.50/3.95 % (3699252)Termination reason: Refutation
% 6.50/3.95 % (3699252)Time elapsed: 0.100 s
% 6.50/3.95 % (3699252)Peak memory usage: 14 MB
% 6.50/3.95 % (3699252)Instructions burned: 161 (million)
% 6.50/3.95 % (3699197)Success in time 3.712 s
% 6.50/3.95 % Vampire exiting
%------------------------------------------------------------------------------