%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG232+1 : 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 : n014.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:30 AM UTC 2026
% Result : Theorem 105.52s 28.10s
% Output : Refutation 194.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 27
% Syntax : Number of formulae : 249 ( 40 unt; 13 def)
% Number of atoms : 937 ( 85 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1310 ( 622 ~; 623 |; 19 &)
% ( 20 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 6 prp; 0-4 aty)
% Number of functors : 26 ( 26 usr; 11 con; 0-5 aty)
% Number of variables : 505 ( 0 sgn 497 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_closure3) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f19,axiom,
! [X0,X1,X2] :
( ( m1_pboole(X1,X0)
& m1_pboole(X2,X0) )
=> k3_pboole(X0,X1,X2) = k3_pboole(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_pboole) ).
fof(f22,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(f23,axiom,
! [X0,X1,X2] :
( X2 = k3_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f24,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m4_pboole(X3,X0,X1)
=> ( X3 = k2_closure3(X0,X1,X2)
<=> ! [X4] :
( r2_hidden(X4,X0)
=> k1_funct_1(X3,X4) = k3_tarski(a_4_0_closure3(X0,X1,X2,X4)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_closure3) ).
fof(f25,axiom,
! [X0,X1] :
( X1 = k3_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_tarski) ).
fof(f26,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_pboole(X2,X0)
=> ( r2_pboole(X0,X1,X2)
<=> ! [X3] :
( r2_hidden(X3,X0)
=> r1_tarski(k1_funct_1(X1,X3),k1_funct_1(X2,X3)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_pboole) ).
fof(f27,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_pboole(X2,X0)
=> ! [X3] :
( m1_pboole(X3,X0)
=> ( X3 = k3_pboole(X0,X1,X2)
<=> ! [X4] :
( r2_hidden(X4,X0)
=> k1_funct_1(X3,X4) = k3_xboole_0(k1_funct_1(X1,X4),k1_funct_1(X2,X4)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_pboole) ).
fof(f32,axiom,
! [X0,X1,X2] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> m4_pboole(k2_closure3(X0,X1,X2),X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_closure3) ).
fof(f33,axiom,
! [X0,X1,X2] :
( ( m1_pboole(X1,X0)
& m1_pboole(X2,X0) )
=> m1_pboole(k3_pboole(X0,X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_pboole) ).
fof(f36,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_closure3) ).
fof(f42,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m4_pboole(X2,X0,X1)
=> m1_pboole(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m4_pboole) ).
fof(f57,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_pboole(X2,X1)
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) )
=> ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
<=> ? [X5] :
( m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
& X0 = k1_funct_1(X5,X4)
& r2_hidden(X5,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_4_0_closure3) ).
fof(f84,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_closure3) ).
fof(f127,plain,
? [X0,X1] :
( ? [X2] :
( ? [X3] :
( ~ r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
& m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f150,plain,
! [X0,X1,X2] :
( k3_pboole(X0,X1,X2) = k3_pboole(X0,X2,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f151,plain,
! [X0,X1,X2] :
( k3_pboole(X0,X1,X2) = k3_pboole(X0,X2,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(flattening,[],[f150]) ).
fof(f154,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f155,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_closure3(X0,X1,X2)
<=> ! [X4] :
( k1_funct_1(X3,X4) = k3_tarski(a_4_0_closure3(X0,X1,X2,X4))
| ~ r2_hidden(X4,X0) ) )
| ~ m4_pboole(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f156,plain,
! [X0,X1] :
( ! [X2] :
( ( r2_pboole(X0,X1,X2)
<=> ! [X3] :
( r1_tarski(k1_funct_1(X1,X3),k1_funct_1(X2,X3))
| ~ r2_hidden(X3,X0) ) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f157,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k3_pboole(X0,X1,X2)
<=> ! [X4] :
( k1_funct_1(X3,X4) = k3_xboole_0(k1_funct_1(X1,X4),k1_funct_1(X2,X4))
| ~ r2_hidden(X4,X0) ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f158,plain,
! [X0,X1,X2] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f32]) ).
fof(f159,plain,
! [X0,X1,X2] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f158]) ).
fof(f160,plain,
! [X0,X1,X2] :
( m1_pboole(k3_pboole(X0,X1,X2),X0)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f161,plain,
! [X0,X1,X2] :
( m1_pboole(k3_pboole(X0,X1,X2),X0)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(flattening,[],[f160]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f36]) ).
fof(f163,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f162]) ).
fof(f170,plain,
! [X0,X1] :
( ! [X2] :
( m1_pboole(X2,X0)
| ~ m4_pboole(X2,X0,X1) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f187,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
<=> ? [X5] :
( m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
& X0 = k1_funct_1(X5,X4)
& r2_hidden(X5,X3) ) )
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(ennf_transformation,[],[f57]) ).
fof(f188,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
<=> ? [X5] :
( m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
& X0 = k1_funct_1(X5,X4)
& r2_hidden(X5,X3) ) )
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(flattening,[],[f187]) ).
fof(f206,plain,
! [X0,X1,X2,X3] :
( k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f84]) ).
fof(f207,plain,
! [X0,X1,X2,X3] :
( k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f206]) ).
fof(f225,plain,
m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f127]) ).
fof(f226,plain,
~ r2_pboole(sK0,k2_closure3(sK0,sK1,k4_closure3(sK0,sK1,sK2,sK3)),k3_pboole(sK0,k2_closure3(sK0,sK1,sK2),k2_closure3(sK0,sK1,sK3))),
inference(cnf_transformation,[],[f127]) ).
fof(f227,plain,
m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f127]) ).
fof(f228,plain,
m1_pboole(sK1,sK0),
inference(cnf_transformation,[],[f127]) ).
fof(f241,plain,
! [X2,X0,X1] :
( k3_pboole(X0,X1,X2) = k3_pboole(X0,X2,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f245,plain,
! [X0,X1] :
( r2_hidden(sK4(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f246,plain,
! [X0,X1] :
( ~ r2_hidden(sK4(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f250,plain,
! [X2,X3,X0,X1] :
( k3_xboole_0(X0,X1) != X2
| ~ r2_hidden(X3,X2)
| r2_hidden(X3,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f251,plain,
! [X2,X3,X0,X1] :
( k3_xboole_0(X0,X1) != X2
| ~ r2_hidden(X3,X2)
| r2_hidden(X3,X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f252,plain,
! [X2,X3,X0,X1] :
( k3_xboole_0(X0,X1) != X2
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X2)
| ~ r2_hidden(X3,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f253,plain,
! [X2,X3,X0,X1,X4] :
( k2_closure3(X0,X1,X2) != X3
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m4_pboole(X3,X0,X1)
| ~ r2_hidden(X4,X0)
| k1_funct_1(X3,X4) = k3_tarski(a_4_0_closure3(X0,X1,X2,X4))
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f259,plain,
! [X2,X0,X1] :
( k3_tarski(X0) != X1
| ~ r2_hidden(X2,X1)
| r2_hidden(sK8(X0,X2),X0) ),
inference(cnf_transformation,[],[f25]) ).
fof(f260,plain,
! [X2,X0,X1] :
( k3_tarski(X0) != X1
| ~ r2_hidden(X2,X1)
| r2_hidden(X2,sK8(X0,X2)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f261,plain,
! [X2,X3,X0,X1] :
( k3_tarski(X0) != X1
| ~ r2_hidden(X2,X3)
| r2_hidden(X2,X1)
| ~ r2_hidden(X3,X0) ),
inference(cnf_transformation,[],[f25]) ).
fof(f263,plain,
! [X2,X0,X1] :
( r2_hidden(sK10(X0,X1,X2),X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0)
| r2_pboole(X0,X1,X2) ),
inference(cnf_transformation,[],[f156]) ).
fof(f264,plain,
! [X2,X0,X1] :
( ~ r1_tarski(k1_funct_1(X1,sK10(X0,X1,X2)),k1_funct_1(X2,sK10(X0,X1,X2)))
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0)
| r2_pboole(X0,X1,X2) ),
inference(cnf_transformation,[],[f156]) ).
fof(f265,plain,
! [X2,X3,X0,X1,X4] :
( k3_pboole(X0,X1,X2) != X3
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X3,X0)
| ~ r2_hidden(X4,X0)
| k1_funct_1(X3,X4) = k3_xboole_0(k1_funct_1(X1,X4),k1_funct_1(X2,X4))
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f268,plain,
! [X2,X0,X1] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f159]) ).
fof(f269,plain,
! [X2,X0,X1] :
( m1_pboole(k3_pboole(X0,X1,X2),X0)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f270,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f163]) ).
fof(f280,plain,
! [X2,X0,X1] :
( ~ m4_pboole(X2,X0,X1)
| ~ m1_pboole(X1,X0)
| m1_pboole(X2,X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f302,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK17(X0,X1,X2,X3,X4),X3)
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f188]) ).
fof(f303,plain,
! [X2,X3,X0,X1,X4] :
( k1_funct_1(sK17(X0,X1,X2,X3,X4),X4) = X0
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f188]) ).
fof(f304,plain,
! [X2,X3,X0,X1,X4] :
( m1_closure2(sK17(X0,X1,X2,X3,X4),X1,X2,k6_closure2(X1,X2))
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f188]) ).
fof(f305,plain,
! [X2,X3,X0,X1,X4,X5] :
( k1_funct_1(X5,X4) != X0
| ~ m1_pboole(X2,X1)
| ~ r2_hidden(X5,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
| r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f188]) ).
fof(f381,plain,
! [X2,X3,X0,X1] :
( k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f207]) ).
fof(f401,definition,
sF42 = k1_closure2(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
fof(f402,plain,
k1_closure2(sK0,sK1) = sF42,
inference(reorient_equations,[],[f401]) ).
fof(f403,definition,
sF43 = k1_zfmisc_1(sF42),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
fof(f404,plain,
k1_zfmisc_1(sF42) = sF43,
inference(reorient_equations,[],[f403]) ).
fof(f405,plain,
m1_subset_1(sK2,sF43),
inference(definition_folding,[],[f227,f404,f402]) ).
fof(f406,definition,
sF44 = k4_closure3(sK0,sK1,sK2,sK3),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
fof(f407,plain,
k4_closure3(sK0,sK1,sK2,sK3) = sF44,
inference(reorient_equations,[],[f406]) ).
fof(f408,definition,
sF45 = k2_closure3(sK0,sK1,sF44),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
fof(f409,plain,
k2_closure3(sK0,sK1,sF44) = sF45,
inference(reorient_equations,[],[f408]) ).
fof(f410,definition,
sF46 = k2_closure3(sK0,sK1,sK2),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f411,plain,
k2_closure3(sK0,sK1,sK2) = sF46,
inference(reorient_equations,[],[f410]) ).
fof(f412,definition,
sF47 = k2_closure3(sK0,sK1,sK3),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
fof(f413,plain,
k2_closure3(sK0,sK1,sK3) = sF47,
inference(reorient_equations,[],[f412]) ).
fof(f414,definition,
sF48 = k3_pboole(sK0,sF46,sF47),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f415,plain,
k3_pboole(sK0,sF46,sF47) = sF48,
inference(reorient_equations,[],[f414]) ).
fof(f416,plain,
~ r2_pboole(sK0,sF45,sF48),
inference(definition_folding,[],[f226,f415,f413,f411,f409,f407]) ).
fof(f417,plain,
m1_subset_1(sK3,sF43),
inference(definition_folding,[],[f225,f404,f402]) ).
fof(f418,definition,
! [X2,X1] : sF49(X1,X2) = k1_zfmisc_1(k1_closure2(X1,X2)),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f419,plain,
! [X2,X1] : k1_zfmisc_1(k1_closure2(X1,X2)) = sF49(X1,X2),
inference(reorient_equations,[],[f418]) ).
fof(f432,plain,
k1_zfmisc_1(sF42) = sF49(sK0,sK1),
inference(superposition,[],[f419,f402]) ).
fof(f433,plain,
sF43 = sF49(sK0,sK1),
inference(forward_demodulation,[],[f432,f404]) ).
fof(f440,plain,
( sF44 = k3_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f407,f381]) ).
fof(f449,plain,
( sF44 = k3_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f440,f228]) ).
fof(f455,plain,
( ~ m1_subset_1(sK2,sF49(sK0,sK1))
| sF44 = k3_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f449,f419]) ).
fof(f459,plain,
( ~ m1_subset_1(sK2,sF43)
| sF44 = k3_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f455,f433]) ).
fof(f461,plain,
( sF44 = k3_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f459,f405]) ).
fof(f463,plain,
( ~ m1_subset_1(sK3,sF49(sK0,sK1))
| sF44 = k3_xboole_0(sK2,sK3) ),
inference(forward_demodulation,[],[f461,f419]) ).
fof(f465,plain,
( ~ m1_subset_1(sK3,sF43)
| sF44 = k3_xboole_0(sK2,sK3) ),
inference(forward_demodulation,[],[f463,f433]) ).
fof(f467,plain,
sF44 = k3_xboole_0(sK2,sK3),
inference(forward_subsumption_resolution,[],[f465,f417]) ).
fof(f475,plain,
( m1_pboole(sF48,sK0)
| ~ m1_pboole(sF46,sK0)
| ~ m1_pboole(sF47,sK0) ),
inference(superposition,[],[f269,f415]) ).
fof(f485,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ m4_pboole(k2_closure3(X1,X2,X0),X1,X2)
| ~ r2_hidden(X3,X1)
| k1_funct_1(k2_closure3(X1,X2,X0),X3) = k3_tarski(a_4_0_closure3(X1,X2,X0,X3))
| ~ m1_pboole(X2,X1) ),
inference(equality_resolution,[],[f253]) ).
fof(f486,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ r2_hidden(X3,X1)
| k1_funct_1(k2_closure3(X1,X2,X0),X3) = k3_tarski(a_4_0_closure3(X1,X2,X0,X3))
| ~ m1_pboole(X2,X1) ),
inference(forward_subsumption_resolution,[],[f485,f268]) ).
fof(f490,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(k2_closure3(X1,X2,X0),X3) = k3_tarski(a_4_0_closure3(X1,X2,X0,X3))
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X0,sF49(X1,X2))
| ~ m1_pboole(X2,X1) ),
inference(forward_demodulation,[],[f486,f419]) ).
fof(f502,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sF44,X0)) = k1_funct_1(sF45,X0)
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ m1_pboole(sK1,sK0) ),
inference(superposition,[],[f490,f409]) ).
fof(f503,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X0)) = k1_funct_1(sF47,X0)
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sK3,sF49(sK0,sK1))
| ~ m1_pboole(sK1,sK0) ),
inference(superposition,[],[f490,f413]) ).
fof(f504,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0)) = k1_funct_1(sF46,X0)
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sK2,sF49(sK0,sK1))
| ~ m1_pboole(sK1,sK0) ),
inference(superposition,[],[f490,f411]) ).
fof(f509,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0)) = k1_funct_1(sF46,X0)
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sK2,sF49(sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f504,f228]) ).
fof(f510,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X0)) = k1_funct_1(sF47,X0)
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sK3,sF49(sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f503,f228]) ).
fof(f511,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sF44,X0)) = k1_funct_1(sF45,X0)
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sF44,sF49(sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f502,f228]) ).
fof(f512,plain,
! [X0] :
( ~ m1_subset_1(sK2,sF43)
| k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0)) = k1_funct_1(sF46,X0)
| ~ r2_hidden(X0,sK0) ),
inference(forward_demodulation,[],[f509,f433]) ).
fof(f513,plain,
! [X0] :
( ~ m1_subset_1(sK3,sF43)
| k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X0)) = k1_funct_1(sF47,X0)
| ~ r2_hidden(X0,sK0) ),
inference(forward_demodulation,[],[f510,f433]) ).
fof(f514,plain,
! [X0] :
( ~ m1_subset_1(sF44,sF43)
| k3_tarski(a_4_0_closure3(sK0,sK1,sF44,X0)) = k1_funct_1(sF45,X0)
| ~ r2_hidden(X0,sK0) ),
inference(forward_demodulation,[],[f511,f433]) ).
fof(f515,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0)) = k1_funct_1(sF46,X0)
| ~ r2_hidden(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f512,f405]) ).
fof(f516,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X0)) = k1_funct_1(sF47,X0)
| ~ r2_hidden(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f513,f417]) ).
fof(f518,definition,
( spl52_1
<=> ! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sF44,X0)) = k1_funct_1(sF45,X0)
| ~ r2_hidden(X0,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl52_1])],[avatar_definition]) ).
fof(f519,plain,
( ! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sF44,X0)) = k1_funct_1(sF45,X0)
| ~ r2_hidden(X0,sK0) )
| ~ spl52_1 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f521,definition,
( spl52_2
<=> m1_subset_1(sF44,sF43) ),
introduced(definition,[new_symbols(definition,[spl52_2])],[avatar_definition]) ).
fof(f522,plain,
( m1_subset_1(sF44,sF43)
| ~ spl52_2 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f523,plain,
( ~ m1_subset_1(sF44,sF43)
| spl52_2 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f524,plain,
( spl52_1
| ~ spl52_2 ),
inference(avatar_split_clause,[],[f514,f521,f518]) ).
fof(f618,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k3_xboole_0(X1,X2))
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X0,X2) ),
inference(equality_resolution,[],[f252]) ).
fof(f629,plain,
! [X2,X3,X0,X1,X4] :
( k3_pboole(X0,X1,X2) != X3
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X3,X0)
| ~ r2_hidden(X4,X0)
| k1_funct_1(X3,X4) = k3_xboole_0(k1_funct_1(X2,X4),k1_funct_1(X1,X4))
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(superposition,[],[f265,f241]) ).
fof(f633,plain,
! [X2,X3,X0,X1,X4] :
( k3_pboole(X0,X1,X2) != X3
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X3,X0)
| ~ r2_hidden(X4,X0)
| k1_funct_1(X3,X4) = k3_xboole_0(k1_funct_1(X2,X4),k1_funct_1(X1,X4))
| ~ m1_pboole(X2,X0) ),
inference(duplicate_literal_removal,[],[f629]) ).
fof(f638,definition,
( spl52_4
<=> m1_pboole(sF46,sK0) ),
introduced(definition,[new_symbols(definition,[spl52_4])],[avatar_definition]) ).
fof(f639,plain,
( m1_pboole(sF46,sK0)
| ~ spl52_4 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f640,plain,
( ~ m1_pboole(sF46,sK0)
| spl52_4 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f642,definition,
( spl52_5
<=> m1_pboole(sF47,sK0) ),
introduced(definition,[new_symbols(definition,[spl52_5])],[avatar_definition]) ).
fof(f651,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k3_tarski(X2))
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X1,X2) ),
inference(equality_resolution,[],[f261]) ).
fof(f704,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X0,X1)
| ~ m1_pboole(k3_pboole(X1,X0,X2),X1)
| ~ r2_hidden(X3,X1)
| k3_xboole_0(k1_funct_1(X2,X3),k1_funct_1(X0,X3)) = k1_funct_1(k3_pboole(X1,X0,X2),X3)
| ~ m1_pboole(X2,X1) ),
inference(equality_resolution,[],[f633]) ).
fof(f708,plain,
! [X2,X3,X0,X1] :
( k3_xboole_0(k1_funct_1(X2,X3),k1_funct_1(X0,X3)) = k1_funct_1(k3_pboole(X1,X0,X2),X3)
| ~ r2_hidden(X3,X1)
| ~ m1_pboole(X0,X1)
| ~ m1_pboole(X2,X1) ),
inference(forward_subsumption_resolution,[],[f704,f269]) ).
fof(f722,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X4,k1_funct_1(k3_pboole(X0,X1,X2),X3))
| ~ r2_hidden(X4,k1_funct_1(X2,X3))
| ~ r2_hidden(X4,k1_funct_1(X1,X3))
| ~ r2_hidden(X3,X0)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(superposition,[],[f618,f708]) ).
fof(f739,plain,
( m1_subset_1(sF44,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f270,f407]) ).
fof(f757,plain,
( m1_subset_1(sF44,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f739,f228]) ).
fof(f766,plain,
( m1_subset_1(sF44,sF49(sK0,sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f757,f419]) ).
fof(f775,plain,
( m1_subset_1(sF44,sF43)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f766,f433]) ).
fof(f778,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| spl52_2 ),
inference(forward_subsumption_resolution,[],[f775,f523]) ).
fof(f780,plain,
( ~ m1_subset_1(sK2,sF49(sK0,sK1))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| spl52_2 ),
inference(forward_demodulation,[],[f778,f419]) ).
fof(f781,plain,
( ~ m1_subset_1(sK2,sF43)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| spl52_2 ),
inference(forward_demodulation,[],[f780,f433]) ).
fof(f782,plain,
( ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| spl52_2 ),
inference(forward_subsumption_resolution,[],[f781,f405]) ).
fof(f783,plain,
( ~ m1_subset_1(sK3,sF49(sK0,sK1))
| spl52_2 ),
inference(forward_demodulation,[],[f782,f419]) ).
fof(f784,plain,
( ~ m1_subset_1(sK3,sF43)
| spl52_2 ),
inference(forward_demodulation,[],[f783,f433]) ).
fof(f785,plain,
( $false
| spl52_2 ),
inference(forward_subsumption_resolution,[],[f784,f417]) ).
fof(f786,plain,
spl52_2,
inference(avatar_contradiction_clause,[],[f785]) ).
fof(f824,plain,
! [X0,X1] :
( sF44 != X0
| ~ r2_hidden(X1,X0)
| r2_hidden(X1,sK3) ),
inference(superposition,[],[f250,f467]) ).
fof(f829,plain,
! [X0] :
( ~ r2_hidden(X0,sF44)
| r2_hidden(X0,sK3) ),
inference(equality_resolution,[],[f824]) ).
fof(f832,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK17(X0,X1,X2,sF44,X3),sK3)
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(sF44,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,sF44,X3)) ),
inference(resolution,[],[f829,f302]) ).
fof(f838,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK17(X0,X1,X2,sF44,X3),sK3)
| ~ m1_subset_1(sF44,sF49(X1,X2))
| ~ m1_pboole(X2,X1)
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,sF44,X3)) ),
inference(forward_demodulation,[],[f832,f419]) ).
fof(f856,plain,
! [X0,X1] :
( sF44 != X0
| ~ r2_hidden(X1,X0)
| r2_hidden(X1,sK2) ),
inference(superposition,[],[f251,f467]) ).
fof(f861,plain,
! [X0] :
( ~ r2_hidden(X0,sF44)
| r2_hidden(X0,sK2) ),
inference(equality_resolution,[],[f856]) ).
fof(f864,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK17(X0,X1,X2,sF44,X3),sK2)
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(sF44,k1_zfmisc_1(k1_closure2(X1,X2)))
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,sF44,X3)) ),
inference(resolution,[],[f861,f302]) ).
fof(f870,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK17(X0,X1,X2,sF44,X3),sK2)
| ~ m1_subset_1(sF44,sF49(X1,X2))
| ~ m1_pboole(X2,X1)
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,sF44,X3)) ),
inference(forward_demodulation,[],[f864,f419]) ).
fof(f873,plain,
( m4_pboole(sF45,sK0,sK1)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sF44,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f268,f409]) ).
fof(f874,plain,
( m4_pboole(sF47,sK0,sK1)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f268,f413]) ).
fof(f875,plain,
( m4_pboole(sF46,sK0,sK1)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f268,f411]) ).
fof(f876,plain,
( m4_pboole(sF46,sK0,sK1)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f875,f228]) ).
fof(f877,plain,
( m4_pboole(sF47,sK0,sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f874,f228]) ).
fof(f878,plain,
( m4_pboole(sF45,sK0,sK1)
| ~ m1_subset_1(sF44,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f873,f228]) ).
fof(f879,plain,
( ~ m1_subset_1(sK2,sF49(sK0,sK1))
| m4_pboole(sF46,sK0,sK1) ),
inference(forward_demodulation,[],[f876,f419]) ).
fof(f880,plain,
( ~ m1_subset_1(sK3,sF49(sK0,sK1))
| m4_pboole(sF47,sK0,sK1) ),
inference(forward_demodulation,[],[f877,f419]) ).
fof(f881,plain,
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| m4_pboole(sF45,sK0,sK1) ),
inference(forward_demodulation,[],[f878,f419]) ).
fof(f882,plain,
( ~ m1_subset_1(sK2,sF43)
| m4_pboole(sF46,sK0,sK1) ),
inference(forward_demodulation,[],[f879,f433]) ).
fof(f883,plain,
( ~ m1_subset_1(sK3,sF43)
| m4_pboole(sF47,sK0,sK1) ),
inference(forward_demodulation,[],[f880,f433]) ).
fof(f884,plain,
( ~ m1_subset_1(sF44,sF43)
| m4_pboole(sF45,sK0,sK1) ),
inference(forward_demodulation,[],[f881,f433]) ).
fof(f885,plain,
m4_pboole(sF46,sK0,sK1),
inference(forward_subsumption_resolution,[],[f882,f405]) ).
fof(f886,plain,
m4_pboole(sF47,sK0,sK1),
inference(forward_subsumption_resolution,[],[f883,f417]) ).
fof(f887,plain,
( m4_pboole(sF45,sK0,sK1)
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f884,f522]) ).
fof(f890,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sK3,X0))
| ~ r2_hidden(X1,X2)
| r2_hidden(X1,k1_funct_1(sF47,X0))
| ~ r2_hidden(X0,sK0) ),
inference(superposition,[],[f651,f516]) ).
fof(f891,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sK2,X0))
| ~ r2_hidden(X1,X2)
| r2_hidden(X1,k1_funct_1(sF46,X0))
| ~ r2_hidden(X0,sK0) ),
inference(superposition,[],[f651,f515]) ).
fof(f989,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_pboole(X0,X1)
| ~ r2_hidden(X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X0)))
| ~ m1_closure2(X2,X1,X0,k6_closure2(X1,X0))
| r2_hidden(k1_funct_1(X2,X4),a_4_0_closure3(X1,X0,X3,X4)) ),
inference(equality_resolution,[],[f305]) ).
fof(f990,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(k1_funct_1(X2,X4),a_4_0_closure3(X1,X0,X3,X4))
| ~ m1_pboole(X0,X1)
| ~ r2_hidden(X2,X3)
| ~ m1_closure2(X2,X1,X0,k6_closure2(X1,X0))
| ~ m1_subset_1(X3,sF49(X1,X0)) ),
inference(forward_demodulation,[],[f989,f419]) ).
fof(f998,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF45,X0) != X1
| ~ r2_hidden(X2,X1)
| r2_hidden(X2,sK8(a_4_0_closure3(sK0,sK1,sF44,X0),X2))
| ~ r2_hidden(X0,sK0) )
| ~ spl52_1 ),
inference(superposition,[],[f260,f519]) ).
fof(f1002,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK8(a_4_0_closure3(sK0,sK1,sF44,X1),X0))
| ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_1 ),
inference(equality_resolution,[],[f998]) ).
fof(f1025,plain,
! [X2,X0,X1] :
( ~ m1_pboole(sK1,sK0)
| ~ r2_hidden(X0,sK3)
| ~ m1_closure2(X0,sK0,sK1,k6_closure2(sK0,sK1))
| ~ m1_subset_1(sK3,sF49(sK0,sK1))
| ~ r2_hidden(X1,k1_funct_1(X0,X2))
| r2_hidden(X1,k1_funct_1(sF47,X2))
| ~ r2_hidden(X2,sK0) ),
inference(resolution,[],[f990,f890]) ).
fof(f1026,plain,
! [X2,X0,X1] :
( ~ m1_pboole(sK1,sK0)
| ~ r2_hidden(X0,sK2)
| ~ m1_closure2(X0,sK0,sK1,k6_closure2(sK0,sK1))
| ~ m1_subset_1(sK2,sF49(sK0,sK1))
| ~ r2_hidden(X1,k1_funct_1(X0,X2))
| r2_hidden(X1,k1_funct_1(sF46,X2))
| ~ r2_hidden(X2,sK0) ),
inference(resolution,[],[f990,f891]) ).
fof(f1033,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,sK2)
| ~ m1_closure2(X0,sK0,sK1,k6_closure2(sK0,sK1))
| ~ m1_subset_1(sK2,sF49(sK0,sK1))
| ~ r2_hidden(X1,k1_funct_1(X0,X2))
| r2_hidden(X1,k1_funct_1(sF46,X2))
| ~ r2_hidden(X2,sK0) ),
inference(forward_subsumption_resolution,[],[f1026,f228]) ).
fof(f1034,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,sK3)
| ~ m1_closure2(X0,sK0,sK1,k6_closure2(sK0,sK1))
| ~ m1_subset_1(sK3,sF49(sK0,sK1))
| ~ r2_hidden(X1,k1_funct_1(X0,X2))
| r2_hidden(X1,k1_funct_1(sF47,X2))
| ~ r2_hidden(X2,sK0) ),
inference(forward_subsumption_resolution,[],[f1025,f228]) ).
fof(f1036,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK2,sF43)
| ~ r2_hidden(X0,sK2)
| ~ m1_closure2(X0,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X1,k1_funct_1(X0,X2))
| r2_hidden(X1,k1_funct_1(sF46,X2))
| ~ r2_hidden(X2,sK0) ),
inference(forward_demodulation,[],[f1033,f433]) ).
fof(f1037,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK3,sF43)
| ~ r2_hidden(X0,sK3)
| ~ m1_closure2(X0,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X1,k1_funct_1(X0,X2))
| r2_hidden(X1,k1_funct_1(sF47,X2))
| ~ r2_hidden(X2,sK0) ),
inference(forward_demodulation,[],[f1034,f433]) ).
fof(f1039,plain,
! [X2,X0,X1] :
( ~ m1_closure2(X0,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,k1_funct_1(X0,X2))
| r2_hidden(X1,k1_funct_1(sF46,X2))
| ~ r2_hidden(X2,sK0) ),
inference(forward_subsumption_resolution,[],[f1036,f405]) ).
fof(f1040,plain,
! [X2,X0,X1] :
( ~ m1_closure2(X0,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X0,sK3)
| ~ r2_hidden(X1,k1_funct_1(X0,X2))
| r2_hidden(X1,k1_funct_1(sF47,X2))
| ~ r2_hidden(X2,sK0) ),
inference(forward_subsumption_resolution,[],[f1037,f417]) ).
fof(f1122,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X0,X2))
| ~ r2_hidden(sK17(X1,sK0,sK1,X0,X2),sK2)
| ~ r2_hidden(X3,k1_funct_1(sK17(X1,sK0,sK1,X0,X2),X4))
| r2_hidden(X3,k1_funct_1(sF46,X4))
| ~ r2_hidden(X4,sK0) ),
inference(resolution,[],[f304,f1039]) ).
fof(f1123,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X0,X2))
| ~ r2_hidden(sK17(X1,sK0,sK1,X0,X2),sK3)
| ~ r2_hidden(X3,k1_funct_1(sK17(X1,sK0,sK1,X0,X2),X4))
| r2_hidden(X3,k1_funct_1(sF47,X4))
| ~ r2_hidden(X4,sK0) ),
inference(resolution,[],[f304,f1040]) ).
fof(f1127,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X0,X2))
| ~ r2_hidden(sK17(X1,sK0,sK1,X0,X2),sK3)
| ~ r2_hidden(X3,k1_funct_1(sK17(X1,sK0,sK1,X0,X2),X4))
| r2_hidden(X3,k1_funct_1(sF47,X4))
| ~ r2_hidden(X4,sK0) ),
inference(forward_subsumption_resolution,[],[f1123,f228]) ).
fof(f1128,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X0,X2))
| ~ r2_hidden(sK17(X1,sK0,sK1,X0,X2),sK2)
| ~ r2_hidden(X3,k1_funct_1(sK17(X1,sK0,sK1,X0,X2),X4))
| r2_hidden(X3,k1_funct_1(sF46,X4))
| ~ r2_hidden(X4,sK0) ),
inference(forward_subsumption_resolution,[],[f1122,f228]) ).
fof(f1130,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X0,sF49(sK0,sK1))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X0,X2))
| ~ r2_hidden(sK17(X1,sK0,sK1,X0,X2),sK3)
| ~ r2_hidden(X3,k1_funct_1(sK17(X1,sK0,sK1,X0,X2),X4))
| r2_hidden(X3,k1_funct_1(sF47,X4))
| ~ r2_hidden(X4,sK0) ),
inference(forward_demodulation,[],[f1127,f419]) ).
fof(f1131,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X0,sF49(sK0,sK1))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X0,X2))
| ~ r2_hidden(sK17(X1,sK0,sK1,X0,X2),sK2)
| ~ r2_hidden(X3,k1_funct_1(sK17(X1,sK0,sK1,X0,X2),X4))
| r2_hidden(X3,k1_funct_1(sF46,X4))
| ~ r2_hidden(X4,sK0) ),
inference(forward_demodulation,[],[f1128,f419]) ).
fof(f1133,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X3,k1_funct_1(sK17(X1,sK0,sK1,X0,X2),X4))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X0,X2))
| ~ r2_hidden(sK17(X1,sK0,sK1,X0,X2),sK3)
| ~ m1_subset_1(X0,sF43)
| r2_hidden(X3,k1_funct_1(sF47,X4))
| ~ r2_hidden(X4,sK0) ),
inference(forward_demodulation,[],[f1130,f433]) ).
fof(f1134,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X3,k1_funct_1(sK17(X1,sK0,sK1,X0,X2),X4))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X0,X2))
| ~ r2_hidden(sK17(X1,sK0,sK1,X0,X2),sK2)
| ~ m1_subset_1(X0,sF43)
| r2_hidden(X3,k1_funct_1(sF46,X4))
| ~ r2_hidden(X4,sK0) ),
inference(forward_demodulation,[],[f1131,f433]) ).
fof(f1157,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF47,X3))
| ~ r2_hidden(X3,sK0)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) ),
inference(superposition,[],[f1133,f303]) ).
fof(f1158,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF47,X3))
| ~ r2_hidden(X3,sK0)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(duplicate_literal_removal,[],[f1157]) ).
fof(f1159,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF47,X3))
| ~ r2_hidden(X3,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f1158,f228]) ).
fof(f1161,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,sF49(sK0,sK1))
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF47,X3))
| ~ r2_hidden(X3,sK0) ),
inference(forward_demodulation,[],[f1159,f419]) ).
fof(f1162,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,sF43)
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF47,X3))
| ~ r2_hidden(X3,sK0) ),
inference(forward_demodulation,[],[f1161,f433]) ).
fof(f1163,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK3)
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF47,X3))
| ~ r2_hidden(X3,sK0) ),
inference(duplicate_literal_removal,[],[f1162]) ).
fof(f1172,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF46,X3))
| ~ r2_hidden(X3,sK0)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) ),
inference(superposition,[],[f1134,f303]) ).
fof(f1173,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF46,X3))
| ~ r2_hidden(X3,sK0)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(duplicate_literal_removal,[],[f1172]) ).
fof(f1174,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF46,X3))
| ~ r2_hidden(X3,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f1173,f228]) ).
fof(f1176,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,sF49(sK0,sK1))
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF46,X3))
| ~ r2_hidden(X3,sK0) ),
inference(forward_demodulation,[],[f1174,f419]) ).
fof(f1177,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,sF43)
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF46,X3))
| ~ r2_hidden(X3,sK0) ),
inference(forward_demodulation,[],[f1176,f433]) ).
fof(f1178,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(sK17(X0,sK0,sK1,X2,X3),sK2)
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_subset_1(X2,sF43)
| r2_hidden(X1,k1_funct_1(sF46,X3))
| ~ r2_hidden(X3,sK0) ),
inference(duplicate_literal_removal,[],[f1177]) ).
fof(f1204,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF45,X0) != X1
| ~ r2_hidden(X2,X1)
| r2_hidden(sK8(a_4_0_closure3(sK0,sK1,sF44,X0),X2),a_4_0_closure3(sK0,sK1,sF44,X0))
| ~ r2_hidden(X0,sK0) )
| ~ spl52_1 ),
inference(superposition,[],[f259,f519]) ).
fof(f1208,plain,
( ! [X0,X1] :
( r2_hidden(sK8(a_4_0_closure3(sK0,sK1,sF44,X1),X0),a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_1 ),
inference(equality_resolution,[],[f1204]) ).
fof(f1308,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(sK4(X0,k1_funct_1(k3_pboole(X1,X2,X3),X4)),k1_funct_1(X3,X4))
| ~ r2_hidden(sK4(X0,k1_funct_1(k3_pboole(X1,X2,X3),X4)),k1_funct_1(X2,X4))
| ~ r2_hidden(X4,X1)
| ~ m1_pboole(X2,X1)
| ~ m1_pboole(X3,X1)
| r1_tarski(X0,k1_funct_1(k3_pboole(X1,X2,X3),X4)) ),
inference(resolution,[],[f722,f246]) ).
fof(f1878,plain,
! [X0,X1] :
( ~ r2_hidden(sK4(X0,k1_funct_1(sF48,X1)),k1_funct_1(sF47,X1))
| ~ r2_hidden(sK4(X0,k1_funct_1(sF48,X1)),k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF46,sK0)
| ~ m1_pboole(sF47,sK0)
| r1_tarski(X0,k1_funct_1(sF48,X1)) ),
inference(superposition,[],[f1308,f415]) ).
fof(f1958,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ m1_pboole(sK1,sK0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ m1_subset_1(sF44,sF43)
| r2_hidden(X2,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0) ),
inference(resolution,[],[f870,f1178]) ).
fof(f1963,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ m1_pboole(sK1,sK0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(sF44,sF43)
| r2_hidden(X2,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0) ),
inference(duplicate_literal_removal,[],[f1958]) ).
fof(f1965,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(sF44,sF43)
| r2_hidden(X2,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0) ),
inference(forward_subsumption_resolution,[],[f1963,f228]) ).
fof(f1966,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1965,f522]) ).
fof(f1967,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF43)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_2 ),
inference(forward_demodulation,[],[f1966,f433]) ).
fof(f1968,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1967,f522]) ).
fof(f1972,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK8(a_4_0_closure3(sK0,sK1,sF44,X1),X2))
| r2_hidden(X0,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X2,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_1
| ~ spl52_2 ),
inference(resolution,[],[f1968,f1208]) ).
fof(f1981,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK8(a_4_0_closure3(sK0,sK1,sF44,X1),X2))
| r2_hidden(X0,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X2,k1_funct_1(sF45,X1)) )
| ~ spl52_1
| ~ spl52_2 ),
inference(duplicate_literal_removal,[],[f1972]) ).
fof(f1987,plain,
( ! [X0,X1] :
( r2_hidden(X0,k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_1
| ~ spl52_2 ),
inference(resolution,[],[f1981,f1002]) ).
fof(f1999,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0)
| r2_hidden(X0,k1_funct_1(sF46,X1)) )
| ~ spl52_1
| ~ spl52_2 ),
inference(duplicate_literal_removal,[],[f1987]) ).
fof(f2003,plain,
( ! [X0,X1] :
( r2_hidden(sK4(k1_funct_1(sF45,X0),X1),k1_funct_1(sF46,X0))
| ~ r2_hidden(X0,sK0)
| r1_tarski(k1_funct_1(sF45,X0),X1) )
| ~ spl52_1
| ~ spl52_2 ),
inference(resolution,[],[f1999,f245]) ).
fof(f2104,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ m1_pboole(sK1,sK0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ m1_subset_1(sF44,sF43)
| r2_hidden(X2,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0) ),
inference(resolution,[],[f838,f1163]) ).
fof(f2110,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ m1_pboole(sK1,sK0)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(sF44,sF43)
| r2_hidden(X2,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0) ),
inference(duplicate_literal_removal,[],[f2104]) ).
fof(f2112,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(sF44,sF43)
| r2_hidden(X2,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0) ),
inference(forward_subsumption_resolution,[],[f2110,f228]) ).
fof(f2113,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF49(sK0,sK1))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2112,f522]) ).
fof(f2114,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF44,sF43)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_2 ),
inference(forward_demodulation,[],[f2113,f433]) ).
fof(f2115,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sF44,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2114,f522]) ).
fof(f2119,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK8(a_4_0_closure3(sK0,sK1,sF44,X1),X2))
| r2_hidden(X0,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X2,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_1
| ~ spl52_2 ),
inference(resolution,[],[f2115,f1208]) ).
fof(f2128,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK8(a_4_0_closure3(sK0,sK1,sF44,X1),X2))
| r2_hidden(X0,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X2,k1_funct_1(sF45,X1)) )
| ~ spl52_1
| ~ spl52_2 ),
inference(duplicate_literal_removal,[],[f2119]) ).
fof(f2134,plain,
( ! [X0,X1] :
( r2_hidden(X0,k1_funct_1(sF47,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl52_1
| ~ spl52_2 ),
inference(resolution,[],[f2128,f1002]) ).
fof(f2146,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0)
| r2_hidden(X0,k1_funct_1(sF47,X1)) )
| ~ spl52_1
| ~ spl52_2 ),
inference(duplicate_literal_removal,[],[f2134]) ).
fof(f2150,plain,
( ! [X0,X1] :
( r2_hidden(sK4(k1_funct_1(sF45,X0),X1),k1_funct_1(sF47,X0))
| ~ r2_hidden(X0,sK0)
| r1_tarski(k1_funct_1(sF45,X0),X1) )
| ~ spl52_1
| ~ spl52_2 ),
inference(resolution,[],[f2146,f245]) ).
fof(f2365,plain,
( ~ m1_pboole(sK1,sK0)
| m1_pboole(sF45,sK0)
| ~ spl52_2 ),
inference(resolution,[],[f280,f887]) ).
fof(f2366,plain,
( ~ m1_pboole(sK1,sK0)
| m1_pboole(sF46,sK0) ),
inference(resolution,[],[f280,f885]) ).
fof(f2367,plain,
( ~ m1_pboole(sK1,sK0)
| m1_pboole(sF47,sK0) ),
inference(resolution,[],[f280,f886]) ).
fof(f2369,plain,
m1_pboole(sF47,sK0),
inference(forward_subsumption_resolution,[],[f2367,f228]) ).
fof(f2370,plain,
m1_pboole(sF46,sK0),
inference(forward_subsumption_resolution,[],[f2366,f228]) ).
fof(f2371,plain,
( m1_pboole(sF45,sK0)
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2365,f228]) ).
fof(f2373,plain,
( $false
| spl52_4 ),
inference(forward_subsumption_resolution,[],[f2370,f640]) ).
fof(f2374,plain,
spl52_4,
inference(avatar_contradiction_clause,[],[f2373]) ).
fof(f2379,plain,
( ! [X0,X1] :
( ~ r2_hidden(sK4(X0,k1_funct_1(sF48,X1)),k1_funct_1(sF47,X1))
| ~ r2_hidden(sK4(X0,k1_funct_1(sF48,X1)),k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF47,sK0)
| r1_tarski(X0,k1_funct_1(sF48,X1)) )
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f1878,f639]) ).
fof(f2382,plain,
( ! [X0,X1] :
( ~ r2_hidden(sK4(X0,k1_funct_1(sF48,X1)),k1_funct_1(sF47,X1))
| ~ r2_hidden(sK4(X0,k1_funct_1(sF48,X1)),k1_funct_1(sF46,X1))
| ~ r2_hidden(X1,sK0)
| r1_tarski(X0,k1_funct_1(sF48,X1)) )
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f2379,f2369]) ).
fof(f2384,plain,
spl52_5,
inference(avatar_split_clause,[],[f2369,f642]) ).
fof(f2409,definition,
( spl52_9
<=> m1_pboole(sF48,sK0) ),
introduced(definition,[new_symbols(definition,[spl52_9])],[avatar_definition]) ).
fof(f2410,plain,
( m1_pboole(sF48,sK0)
| ~ spl52_9 ),
inference(avatar_component_clause,[],[f2409]) ).
fof(f2416,plain,
( ! [X0] :
( ~ r2_hidden(sK4(k1_funct_1(sF45,X0),k1_funct_1(sF48,X0)),k1_funct_1(sF46,X0))
| ~ r2_hidden(X0,sK0)
| r1_tarski(k1_funct_1(sF45,X0),k1_funct_1(sF48,X0))
| ~ r2_hidden(X0,sK0)
| r1_tarski(k1_funct_1(sF45,X0),k1_funct_1(sF48,X0)) )
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4 ),
inference(resolution,[],[f2382,f2150]) ).
fof(f2419,plain,
( ! [X0] :
( ~ r2_hidden(sK4(k1_funct_1(sF45,X0),k1_funct_1(sF48,X0)),k1_funct_1(sF46,X0))
| ~ r2_hidden(X0,sK0)
| r1_tarski(k1_funct_1(sF45,X0),k1_funct_1(sF48,X0)) )
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4 ),
inference(duplicate_literal_removal,[],[f2416]) ).
fof(f2420,plain,
( ! [X0] :
( r1_tarski(k1_funct_1(sF45,X0),k1_funct_1(sF48,X0))
| ~ r2_hidden(X0,sK0) )
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4 ),
inference(forward_subsumption_resolution,[],[f2419,f2003]) ).
fof(f2426,plain,
( ! [X0] :
( ~ r2_hidden(sK10(X0,sF45,sF48),sK0)
| ~ m1_pboole(sF48,X0)
| ~ m1_pboole(sF45,X0)
| r2_pboole(X0,sF45,sF48) )
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4 ),
inference(resolution,[],[f2420,f264]) ).
fof(f2428,plain,
( ~ m1_pboole(sF48,sK0)
| ~ m1_pboole(sF45,sK0)
| r2_pboole(sK0,sF45,sF48)
| ~ m1_pboole(sF48,sK0)
| ~ m1_pboole(sF45,sK0)
| r2_pboole(sK0,sF45,sF48)
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4 ),
inference(resolution,[],[f2426,f263]) ).
fof(f2429,plain,
( ~ m1_pboole(sF48,sK0)
| ~ m1_pboole(sF45,sK0)
| r2_pboole(sK0,sF45,sF48)
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4 ),
inference(duplicate_literal_removal,[],[f2428]) ).
fof(f3407,plain,
( ~ spl52_5
| ~ spl52_4
| spl52_9 ),
inference(avatar_split_clause,[],[f475,f2409,f638,f642]) ).
fof(f3408,plain,
( ~ m1_pboole(sF45,sK0)
| r2_pboole(sK0,sF45,sF48)
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4
| ~ spl52_9 ),
inference(forward_subsumption_resolution,[],[f2429,f2410]) ).
fof(f3410,plain,
( r2_pboole(sK0,sF45,sF48)
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4
| ~ spl52_9 ),
inference(forward_subsumption_resolution,[],[f3408,f2371]) ).
fof(f3412,plain,
( $false
| ~ spl52_1
| ~ spl52_2
| ~ spl52_4
| ~ spl52_9 ),
inference(forward_subsumption_resolution,[],[f3410,f416]) ).
fof(f3413,plain,
( ~ spl52_1
| ~ spl52_2
| ~ spl52_4
| ~ spl52_9 ),
inference(avatar_contradiction_clause,[],[f3412]) ).
cnf(s1,plain,
( spl52_1
| ~ spl52_2 ),
inference(sat_conversion,[],[f524]) ).
cnf(s4,plain,
spl52_2,
inference(sat_conversion,[],[f786]) ).
cnf(s6,plain,
spl52_4,
inference(sat_conversion,[],[f2374]) ).
cnf(s8,plain,
spl52_5,
inference(sat_conversion,[],[f2384]) ).
cnf(s18,plain,
( ~ spl52_4
| ~ spl52_5
| spl52_9 ),
inference(sat_conversion,[],[f3407]) ).
cnf(s19,plain,
( ~ spl52_1
| ~ spl52_2
| ~ spl52_4
| ~ spl52_9 ),
inference(sat_conversion,[],[f3413]) ).
cnf(s20,plain,
spl52_9,
inference(rat,[],[s18,s8,s6]) ).
cnf(s23,plain,
~ spl52_1,
inference(rat,[],[s19,s20,s6,s4]) ).
cnf(s25,plain,
$false,
inference(rat,[],[s1,s4,s23]) ).
fof(f3414,plain,
$false,
inference(avatar_sat_refutation,[],[s25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG232+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n014.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:55:01 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 10.62/2.16 % (2110223)Detected formulas, will run a generic FOF schedule.
% 10.62/2.16 % (2110232)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=916823115:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.62/2.16 % (2110230)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=328592065:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.62/2.16 % (2110232)Instruction limit reached!
% 10.62/2.16 % (2110232)------------------------------
% 10.62/2.16 % (2110232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.16 % (2110232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.16 % (2110232)CaDiCaL version: 2.1.3
% 10.62/2.16 % (2110232)Termination reason: Instruction limit
% 10.62/2.16 % (2110232)Termination phase: Saturation
% 10.62/2.16 % (2110232)Time elapsed: 0.041 s
% 10.62/2.16 % (2110232)Peak memory usage: 89 MB
% 10.62/2.16 % (2110232)Instructions burned: 122 (million)
% 10.62/2.16 % (2110234)dis-21_1_sil=8000:lcm=predicate:random_seed=384615075:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.62/2.16 % (2110231)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1531430379:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.62/2.16 % (2110229)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=192342603:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.62/2.16 % (2110233)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1542549635:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.62/2.16 % (2110228)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=2577185851:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.62/2.16 % (2110231)Refutation not found, incomplete strategy
% 10.62/2.16 % (2110231)------------------------------
% 10.62/2.16 % (2110231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.16 % (2110231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.16 % (2110231)CaDiCaL version: 2.1.3
% 10.62/2.16 % (2110231)Termination reason: Refutation not found, incomplete strategy
% 10.62/2.16 % (2110231)Time elapsed: 0.003 s
% 10.62/2.16 % (2110231)Peak memory usage: 88 MB
% 10.62/2.16 % (2110231)Instructions burned: 3 (million)
% 10.62/2.16 % (2110234)Instruction limit reached!
% 10.62/2.16 % (2110234)------------------------------
% 10.62/2.16 % (2110234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.16 % (2110234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.16 % (2110234)CaDiCaL version: 2.1.3
% 10.62/2.16 % (2110234)Termination reason: Instruction limit
% 10.62/2.16 % (2110234)Termination phase: Saturation
% 10.62/2.16 % (2110234)Time elapsed: 0.075 s
% 10.62/2.16 % (2110234)Peak memory usage: 90 MB
% 10.62/2.16 % (2110234)Instructions burned: 130 (million)
% 10.62/2.16 % (2110233)Instruction limit reached!
% 10.62/2.16 % (2110233)------------------------------
% 10.62/2.16 % (2110233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.16 % (2110233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.16 % (2110233)CaDiCaL version: 2.1.3
% 10.62/2.16 % (2110233)Termination reason: Instruction limit
% 10.62/2.16 % (2110233)Termination phase: Saturation
% 10.62/2.16 % (2110233)Time elapsed: 0.095 s
% 10.62/2.16 % (2110233)Peak memory usage: 90 MB
% 10.62/2.16 % (2110233)Instructions burned: 140 (million)
% 10.62/2.16 % (2110242)lrs+10_1_sil=8000:sp=occurrence:random_seed=1919165855:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.62/2.16 % (2110243)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1449802154:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.62/2.16 % (2110243)Instruction limit reached!
% 10.62/2.16 % (2110243)------------------------------
% 10.62/2.16 % (2110243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.16 % (2110243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.16 % (2110243)CaDiCaL version: 2.1.3
% 10.62/2.16 % (2110243)Termination reason: Instruction limit
% 10.62/2.16 % (2110243)Termination phase: Saturation
% 15.08/3.03 % (2110243)Time elapsed: 0.040 s
% 15.08/3.03 % (2110243)Peak memory usage: 89 MB
% 15.08/3.03 % (2110243)Instructions burned: 158 (million)
% 15.08/3.03 % (2110244)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3494166825:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.08/3.03 % (2110231)------------------------------
% 15.08/3.03 % (2110231)------------------------------
% 15.08/3.03 % (2110247)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=3623203386:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 15.08/3.03 % (2110242)Instruction limit reached!
% 15.08/3.03 % (2110242)------------------------------
% 15.08/3.03 % (2110242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.08/3.03 % (2110242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.08/3.03 % (2110242)CaDiCaL version: 2.1.3
% 15.08/3.03 % (2110242)Termination reason: Instruction limit
% 15.08/3.03 % (2110242)Termination phase: Saturation
% 15.08/3.03 % (2110242)Time elapsed: 0.182 s
% 15.08/3.03 % (2110242)Peak memory usage: 92 MB
% 15.08/3.03 % (2110242)Instructions burned: 285 (million)
% 15.08/3.03 % (2110247)Instruction limit reached!
% 15.08/3.03 % (2110247)------------------------------
% 15.08/3.03 % (2110247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.08/3.03 % (2110247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.08/3.03 % (2110247)CaDiCaL version: 2.1.3
% 15.08/3.03 % (2110247)Termination reason: Instruction limit
% 15.08/3.03 % (2110247)Termination phase: Saturation
% 15.08/3.03 % (2110247)Time elapsed: 0.075 s
% 15.08/3.03 % (2110247)Peak memory usage: 92 MB
% 15.08/3.03 % (2110247)Instructions burned: 248 (million)
% 15.08/3.03 % (2110249)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3418807251:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 15.08/3.03 % (2110244)Instruction limit reached!
% 15.08/3.03 % (2110244)------------------------------
% 15.08/3.03 % (2110244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.08/3.03 % (2110244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.08/3.03 % (2110244)CaDiCaL version: 2.1.3
% 15.08/3.03 % (2110244)Termination reason: Instruction limit
% 15.08/3.03 % (2110244)Termination phase: Saturation
% 15.08/3.03 % (2110244)Time elapsed: 0.208 s
% 15.08/3.03 % (2110244)Peak memory usage: 93 MB
% 15.08/3.03 % (2110244)Instructions burned: 326 (million)
% 15.08/3.03 % (2110252)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=572827417:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 15.08/3.03 % (2110251)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1919443155:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 15.08/3.03 % (2110252)Instruction limit reached!
% 15.08/3.03 % (2110252)------------------------------
% 15.08/3.03 % (2110252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.08/3.03 % (2110252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.08/3.03 % (2110252)CaDiCaL version: 2.1.3
% 15.08/3.03 % (2110252)Termination reason: Instruction limit
% 15.08/3.03 % (2110252)Termination phase: Saturation
% 15.08/3.03 % (2110252)Time elapsed: 0.041 s
% 15.08/3.03 % (2110252)Peak memory usage: 90 MB
% 15.08/3.03 % (2110252)Instructions burned: 115 (million)
% 15.08/3.03 % (2110249)Instruction limit reached!
% 15.08/3.03 % (2110249)------------------------------
% 15.08/3.03 % (2110249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.08/3.03 % (2110249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.08/3.03 % (2110249)CaDiCaL version: 2.1.3
% 15.08/3.03 % (2110249)Termination reason: Instruction limit
% 15.08/3.03 % (2110249)Termination phase: Saturation
% 15.08/3.03 % (2110249)Time elapsed: 0.152 s
% 15.08/3.03 % (2110249)Peak memory usage: 89 MB
% 15.08/3.03 % (2110249)Instructions burned: 294 (million)
% 15.08/3.03 % (2110257)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=260837797:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 15.08/3.03 % (2110254)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1759968074:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 15.08/3.03 % (2110257)Instruction limit reached!
% 15.08/3.03 % (2110257)------------------------------
% 15.08/3.03 % (2110257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/8.25 % (2110257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.25 % (2110257)CaDiCaL version: 2.1.3
% 53.83/8.25 % (2110257)Termination reason: Instruction limit
% 53.83/8.25 % (2110257)Termination phase: Saturation
% 53.83/8.25 % (2110257)Time elapsed: 0.038 s
% 53.83/8.25 % (2110257)Peak memory usage: 89 MB
% 53.83/8.25 % (2110257)Instructions burned: 114 (million)
% 53.83/8.25 % (2110254)Instruction limit reached!
% 53.83/8.25 % (2110254)------------------------------
% 53.83/8.25 % (2110254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/8.25 % (2110254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.25 % (2110254)CaDiCaL version: 2.1.3
% 53.83/8.25 % (2110254)Termination reason: Instruction limit
% 53.83/8.25 % (2110254)Termination phase: Saturation
% 53.83/8.25 % (2110254)Time elapsed: 0.066 s
% 53.83/8.25 % (2110254)Peak memory usage: 89 MB
% 53.83/8.25 % (2110254)Instructions burned: 127 (million)
% 53.83/8.25 % (2110258)lrs+10_1_sil=8000:sp=occurrence:random_seed=3817068018:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 53.83/8.25 % (2110261)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2136919701:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 53.83/8.25 % (2110261)Refutation not found, incomplete strategy
% 53.83/8.25 % (2110261)------------------------------
% 53.83/8.25 % (2110261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/8.25 % (2110261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.25 % (2110261)CaDiCaL version: 2.1.3
% 53.83/8.25 % (2110261)Termination reason: Refutation not found, incomplete strategy
% 53.83/8.25 % (2110261)Time elapsed: 0.005 s
% 53.83/8.25 % (2110261)Peak memory usage: 89 MB
% 53.83/8.25 % (2110261)Instructions burned: 13 (million)
% 53.83/8.25 % (2110262)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3570836855:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 53.83/8.25 % (2110261)------------------------------
% 53.83/8.25 % (2110261)------------------------------
% 53.83/8.25 % (2110266)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1171481090:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 53.83/8.25 % (2110266)Instruction limit reached!
% 53.83/8.25 % (2110266)------------------------------
% 53.83/8.25 % (2110266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/8.25 % (2110266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.25 % (2110266)CaDiCaL version: 2.1.3
% 53.83/8.25 % (2110266)Termination reason: Instruction limit
% 53.83/8.25 % (2110266)Termination phase: Saturation
% 53.83/8.25 % (2110266)Time elapsed: 0.040 s
% 53.83/8.25 % (2110266)Peak memory usage: 91 MB
% 53.83/8.25 % (2110266)Instructions burned: 135 (million)
% 53.83/8.25 % (2110268)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=482228744:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 53.83/8.25 % (2110258)Instruction limit reached!
% 53.83/8.25 % (2110258)------------------------------
% 53.83/8.25 % (2110258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/8.25 % (2110258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.25 % (2110258)CaDiCaL version: 2.1.3
% 53.83/8.25 % (2110258)Termination reason: Instruction limit
% 53.83/8.25 % (2110258)Termination phase: Saturation
% 53.83/8.25 % (2110258)Time elapsed: 0.531 s
% 53.83/8.25 % (2110258)Peak memory usage: 98 MB
% 53.83/8.25 % (2110258)Instructions burned: 907 (million)
% 53.83/8.25 % (2110268)Instruction limit reached!
% 53.83/8.25 % (2110268)------------------------------
% 53.83/8.25 % (2110268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/8.25 % (2110268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.25 % (2110268)CaDiCaL version: 2.1.3
% 53.83/8.25 % (2110268)Termination reason: Instruction limit
% 53.83/8.25 % (2110268)Termination phase: Saturation
% 53.83/8.25 % (2110268)Time elapsed: 0.181 s
% 53.83/8.25 % (2110268)Peak memory usage: 93 MB
% 53.83/8.25 % (2110268)Instructions burned: 593 (million)
% 53.83/8.25 % (2110270)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1582850683:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 53.83/8.25 % (2110271)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=3526121573:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 70.32/10.67 % (2110271)Instruction limit reached!
% 70.32/10.67 % (2110271)------------------------------
% 70.32/10.67 % (2110271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.32/10.67 % (2110271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.32/10.67 % (2110271)CaDiCaL version: 2.1.3
% 70.32/10.67 % (2110271)Termination reason: Instruction limit
% 70.32/10.67 % (2110271)Termination phase: Saturation
% 70.32/10.67 % (2110271)Time elapsed: 0.045 s
% 70.32/10.67 % (2110271)Peak memory usage: 91 MB
% 70.32/10.67 % (2110271)Instructions burned: 125 (million)
% 70.32/10.67 % (2110274)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1897854237:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 70.32/10.67 % (2110274)Instruction limit reached!
% 70.32/10.67 % (2110274)------------------------------
% 70.32/10.67 % (2110274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.32/10.67 % (2110274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.32/10.67 % (2110274)CaDiCaL version: 2.1.3
% 70.32/10.67 % (2110274)Termination reason: Instruction limit
% 70.32/10.67 % (2110274)Termination phase: Saturation
% 70.32/10.67 % (2110274)Time elapsed: 0.049 s
% 70.32/10.67 % (2110274)Peak memory usage: 90 MB
% 70.32/10.67 % (2110274)Instructions burned: 136 (million)
% 70.32/10.67 % (2110276)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2850985035:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 70.32/10.67 % (2110276)Instruction limit reached!
% 70.32/10.67 % (2110276)------------------------------
% 70.32/10.67 % (2110276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.32/10.67 % (2110276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.32/10.67 % (2110276)CaDiCaL version: 2.1.3
% 70.32/10.67 % (2110276)Termination reason: Instruction limit
% 70.32/10.67 % (2110276)Termination phase: Saturation
% 70.32/10.67 % (2110276)Time elapsed: 0.040 s
% 70.32/10.67 % (2110276)Peak memory usage: 91 MB
% 70.32/10.67 % (2110276)Instructions burned: 143 (million)
% 70.32/10.67 % (2110278)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=25124415:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 70.32/10.67 % (2110278)Instruction limit reached!
% 70.32/10.67 % (2110278)------------------------------
% 70.32/10.67 % (2110278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.32/10.67 % (2110278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.32/10.67 % (2110278)CaDiCaL version: 2.1.3
% 70.32/10.67 % (2110278)Termination reason: Instruction limit
% 70.32/10.67 % (2110278)Termination phase: Saturation
% 70.32/10.67 % (2110278)Time elapsed: 0.142 s
% 70.32/10.67 % (2110278)Peak memory usage: 92 MB
% 70.32/10.67 % (2110278)Instructions burned: 431 (million)
% 70.32/10.67 % (2110280)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=488233757:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi)
% 70.32/10.67 % (2110251)Instruction limit reached!
% 70.32/10.67 % (2110251)------------------------------
% 70.32/10.67 % (2110251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.32/10.67 % (2110251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.32/10.67 % (2110251)CaDiCaL version: 2.1.3
% 70.32/10.67 % (2110251)Termination reason: Instruction limit
% 70.32/10.67 % (2110251)Termination phase: Saturation
% 70.32/10.67 % (2110251)Time elapsed: 1.525 s
% 70.32/10.67 % (2110251)Peak memory usage: 142 MB
% 70.32/10.67 % (2110251)Instructions burned: 2350 (million)
% 70.32/10.67 % (2110282)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=1589833875:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 70.32/10.67 % (2110282)Instruction limit reached!
% 70.32/10.67 % (2110282)------------------------------
% 70.32/10.67 % (2110282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.32/10.67 % (2110282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.32/10.67 % (2110282)CaDiCaL version: 2.1.3
% 97.13/14.39 % (2110282)Termination reason: Instruction limit
% 97.13/14.39 % (2110282)Termination phase: Saturation
% 97.13/14.39 % (2110282)Time elapsed: 0.092 s
% 97.13/14.39 % (2110282)Peak memory usage: 92 MB
% 97.13/14.39 % (2110282)Instructions burned: 151 (million)
% 97.13/14.39 % (2110284)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3607002721:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi)
% 97.13/14.39 % (2110262)Instruction limit reached!
% 97.13/14.39 % (2110262)------------------------------
% 97.13/14.39 % (2110262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.13/14.39 % (2110262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.13/14.39 % (2110262)CaDiCaL version: 2.1.3
% 97.13/14.39 % (2110262)Termination reason: Instruction limit
% 97.13/14.39 % (2110262)Termination phase: Saturation
% 97.13/14.39 % (2110262)Time elapsed: 3.085 s
% 97.13/14.39 % (2110262)Peak memory usage: 163 MB
% 97.13/14.39 % (2110262)Instructions burned: 5203 (million)
% 97.13/14.39 % (2110286)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3191653902:i=667:av=off:fsr=off_2959 on theBenchmark for (2959ds/667Mi)
% 97.13/14.39 % (2110280)Instruction limit reached!
% 97.13/14.39 % (2110280)------------------------------
% 97.13/14.39 % (2110280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.13/14.39 % (2110280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.13/14.39 % (2110280)CaDiCaL version: 2.1.3
% 97.13/14.39 % (2110280)Termination reason: Instruction limit
% 97.13/14.39 % (2110280)Termination phase: Saturation
% 97.13/14.39 % (2110280)Time elapsed: 2.141 s
% 97.13/14.39 % (2110280)Peak memory usage: 173 MB
% 97.13/14.39 % (2110280)Instructions burned: 6060 (million)
% 97.13/14.39 % (2110288)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=356897991:s2a=on:i=185:s2at=1.8:fdi=4_2957 on theBenchmark for (2957ds/185Mi)
% 97.13/14.39 % (2110288)Instruction limit reached!
% 97.13/14.39 % (2110288)------------------------------
% 97.13/14.39 % (2110288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.13/14.39 % (2110288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.13/14.39 % (2110288)CaDiCaL version: 2.1.3
% 97.13/14.39 % (2110288)Termination reason: Instruction limit
% 97.13/14.39 % (2110288)Termination phase: Saturation
% 97.13/14.39 % (2110288)Time elapsed: 0.053 s
% 97.13/14.39 % (2110288)Peak memory usage: 91 MB
% 97.13/14.39 % (2110288)Instructions burned: 188 (million)
% 97.13/14.39 % (2110286)Instruction limit reached!
% 97.13/14.39 % (2110286)------------------------------
% 97.13/14.39 % (2110286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.13/14.39 % (2110286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.13/14.39 % (2110286)CaDiCaL version: 2.1.3
% 97.13/14.39 % (2110286)Termination reason: Instruction limit
% 97.13/14.39 % (2110286)Termination phase: Saturation
% 97.13/14.39 % (2110286)Time elapsed: 0.324 s
% 97.13/14.39 % (2110286)Peak memory usage: 109 MB
% 97.13/14.39 % (2110286)Instructions burned: 668 (million)
% 97.13/14.39 % (2110290)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2249146081:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2955 on theBenchmark for (2955ds/193Mi)
% 97.13/14.39 % (2110290)Instruction limit reached!
% 97.13/14.39 % (2110290)------------------------------
% 97.13/14.39 % (2110290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.13/14.39 % (2110290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.13/14.39 % (2110290)CaDiCaL version: 2.1.3
% 97.13/14.39 % (2110290)Termination reason: Instruction limit
% 97.13/14.39 % (2110290)Termination phase: Saturation
% 97.13/14.39 % (2110290)Time elapsed: 0.065 s
% 97.13/14.39 % (2110290)Peak memory usage: 92 MB
% 97.13/14.39 % (2110290)Instructions burned: 194 (million)
% 97.13/14.39 % (2110291)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=770517484:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2955 on theBenchmark for (2955ds/4850Mi)
% 97.13/14.39 % (2110293)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2793216088:i=12111:sd=1:ss=included_2954 on theBenchmark for (2954ds/12111Mi)
% 97.13/14.39 % (2110291)Instruction limit reached!
% 97.13/14.39 % (2110291)------------------------------
% 97.13/14.39 % (2110291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.69/18.68 % (2110291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.69/18.68 % (2110291)CaDiCaL version: 2.1.3
% 127.69/18.68 % (2110291)Termination reason: Instruction limit
% 127.69/18.68 % (2110291)Termination phase: Saturation
% 127.69/18.68 % (2110291)Time elapsed: 2.957 s
% 127.69/18.68 % (2110291)Peak memory usage: 157 MB
% 127.69/18.68 % (2110291)Instructions burned: 4851 (million)
% 127.69/18.68 % (2110448)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3978750837:i=319:kws=precedence:fsr=off_2924 on theBenchmark for (2924ds/319Mi)
% 127.69/18.68 % (2110448)Instruction limit reached!
% 127.69/18.68 % (2110448)------------------------------
% 127.69/18.68 % (2110448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.69/18.68 % (2110448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.69/18.68 % (2110448)CaDiCaL version: 2.1.3
% 127.69/18.68 % (2110448)Termination reason: Instruction limit
% 127.69/18.68 % (2110448)Termination phase: Saturation
% 127.69/18.68 % (2110448)Time elapsed: 0.182 s
% 127.69/18.68 % (2110448)Peak memory usage: 93 MB
% 127.69/18.68 % (2110448)Instructions burned: 320 (million)
% 127.69/18.68 % (2110450)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1601482413:i=2064:ep=RST_2920 on theBenchmark for (2920ds/2064Mi)
% 127.69/18.68 % (2110293)Instruction limit reached!
% 127.69/18.68 % (2110293)------------------------------
% 127.69/18.68 % (2110293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.69/18.68 % (2110293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.69/18.68 % (2110293)CaDiCaL version: 2.1.3
% 127.69/18.68 % (2110293)Termination reason: Instruction limit
% 127.69/18.68 % (2110293)Termination phase: Saturation
% 127.69/18.68 % (2110293)Time elapsed: 3.917 s
% 127.69/18.68 % (2110293)Peak memory usage: 243 MB
% 127.69/18.68 % (2110293)Instructions burned: 12113 (million)
% 127.69/18.68 % (2110452)dis-1011_128_sil=32000:random_seed=1592818434:i=3706:ep=RST:av=off_2914 on theBenchmark for (2914ds/3706Mi)
% 127.69/18.68 % (2110450)Instruction limit reached!
% 127.69/18.68 % (2110450)------------------------------
% 127.69/18.68 % (2110450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.69/18.68 % (2110450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.69/18.68 % (2110450)CaDiCaL version: 2.1.3
% 127.69/18.68 % (2110450)Termination reason: Instruction limit
% 127.69/18.68 % (2110450)Termination phase: Saturation
% 127.69/18.68 % (2110450)Time elapsed: 1.063 s
% 127.69/18.68 % (2110450)Peak memory usage: 124 MB
% 127.69/18.68 % (2110450)Instructions burned: 2065 (million)
% 127.69/18.68 % (2110454)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2347837920:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2909 on theBenchmark for (2909ds/757Mi)
% 127.69/18.68 % (2110270)Instruction limit reached!
% 127.69/18.68 % (2110270)------------------------------
% 127.69/18.68 % (2110270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.69/18.68 % (2110270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.69/18.68 % (2110270)CaDiCaL version: 2.1.3
% 127.69/18.68 % (2110270)Termination reason: Instruction limit
% 127.69/18.68 % (2110270)Termination phase: Saturation
% 127.69/18.68 % (2110270)Time elapsed: 8.069 s
% 127.69/18.68 % (2110270)Peak memory usage: 240 MB
% 127.69/18.68 % (2110270)Instructions burned: 13194 (million)
% 127.69/18.68 % (2110456)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=148742350:i=13913:ss=axioms:sgt=8_2904 on theBenchmark for (2904ds/13913Mi)
% 127.69/18.68 % (2110454)Instruction limit reached!
% 127.69/18.68 % (2110454)------------------------------
% 127.69/18.68 % (2110454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.69/18.68 % (2110454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.69/18.68 % (2110454)CaDiCaL version: 2.1.3
% 127.69/18.68 % (2110454)Termination reason: Instruction limit
% 127.69/18.68 % (2110454)Termination phase: Saturation
% 127.69/18.68 % (2110454)Time elapsed: 0.488 s
% 127.69/18.68 % (2110454)Peak memory usage: 108 MB
% 127.69/18.68 % (2110454)Instructions burned: 757 (million)
% 127.69/18.68 % (2110458)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3258308741:i=9925:aac=none_2902 on theBenchmark for (2902ds/9925Mi)
% 127.69/18.68 % (2110452)Instruction limit reached!
% 127.69/18.68 % (2110452)------------------------------
% 127.69/18.68 % (2110452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.67/22.47 % (2110452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.67/22.47 % (2110452)CaDiCaL version: 2.1.3
% 154.67/22.47 % (2110452)Termination reason: Instruction limit
% 154.67/22.47 % (2110452)Termination phase: Saturation
% 154.67/22.47 % (2110452)Time elapsed: 1.320 s
% 154.67/22.47 % (2110452)Peak memory usage: 118 MB
% 154.67/22.47 % (2110452)Instructions burned: 3706 (million)
% 154.67/22.47 % (2110460)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3803803911:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2899 on theBenchmark for (2899ds/2479Mi)
% 154.67/22.47 % (2110460)Refutation not found, incomplete strategy
% 154.67/22.47 % (2110460)------------------------------
% 154.67/22.47 % (2110460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.67/22.47 % (2110460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.67/22.47 % (2110460)CaDiCaL version: 2.1.3
% 154.67/22.47 % (2110460)Termination reason: Refutation not found, incomplete strategy
% 154.67/22.47 % (2110460)Time elapsed: 0.003 s
% 154.67/22.47 % (2110460)Peak memory usage: 89 MB
% 154.67/22.47 % (2110460)Instructions burned: 7 (million)
% 154.67/22.47 % (2110460)------------------------------
% 154.67/22.47 % (2110460)------------------------------
% 154.67/22.47 % (2110462)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1236374679:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2897 on theBenchmark for (2897ds/440Mi)
% 154.67/22.47 % (2110462)Instruction limit reached!
% 154.67/22.47 % (2110462)------------------------------
% 154.67/22.47 % (2110462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.67/22.47 % (2110462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.67/22.47 % (2110462)CaDiCaL version: 2.1.3
% 154.67/22.47 % (2110462)Termination reason: Instruction limit
% 154.67/22.47 % (2110462)Termination phase: Saturation
% 154.67/22.47 % (2110462)Time elapsed: 0.135 s
% 154.67/22.47 % (2110462)Peak memory usage: 94 MB
% 154.67/22.47 % (2110462)Instructions burned: 442 (million)
% 154.67/22.47 % (2110464)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3252365058:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2895 on theBenchmark for (2895ds/11145Mi)
% 154.67/22.47 % (2110284)Instruction limit reached!
% 154.67/22.47 % (2110284)------------------------------
% 154.67/22.47 % (2110284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.67/22.47 % (2110284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.67/22.47 % (2110284)CaDiCaL version: 2.1.3
% 154.67/22.47 % (2110284)Termination reason: Instruction limit
% 154.67/22.47 % (2110284)Termination phase: Saturation
% 154.67/22.47 % (2110284)Time elapsed: 8.786 s
% 154.67/22.47 % (2110284)Peak memory usage: 228 MB
% 154.67/22.47 % (2110284)Instructions burned: 14155 (million)
% 154.67/22.47 % (2110466)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=759343719:cts=off:i=3034:av=off:er=known:fsd=on_2887 on theBenchmark for (2887ds/3034Mi)
% 154.67/22.47 % (2110466)Instruction limit reached!
% 154.67/22.47 % (2110466)------------------------------
% 154.67/22.47 % (2110466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.67/22.47 % (2110466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.67/22.47 % (2110466)CaDiCaL version: 2.1.3
% 154.67/22.47 % (2110466)Termination reason: Instruction limit
% 154.67/22.47 % (2110466)Termination phase: Saturation
% 154.67/22.47 % (2110466)Time elapsed: 1.791 s
% 154.67/22.47 % (2110466)Peak memory usage: 141 MB
% 154.67/22.47 % (2110466)Instructions burned: 3035 (million)
% 154.67/22.47 % (2110621)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2116893810:st=2:s2a=on:i=524:s2at=2:ss=axioms_2867 on theBenchmark for (2867ds/524Mi)
% 154.67/22.47 % (2110621)Instruction limit reached!
% 154.67/22.47 % (2110621)------------------------------
% 154.67/22.47 % (2110621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.67/22.47 % (2110621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.67/22.47 % (2110621)CaDiCaL version: 2.1.3
% 154.67/22.47 % (2110621)Termination reason: Instruction limit
% 154.67/22.47 % (2110621)Termination phase: Saturation
% 154.67/22.47 % (2110621)Time elapsed: 0.263 s
% 154.67/22.47 % (2110621)Peak memory usage: 92 MB
% 154.67/22.47 % (2110621)Instructions burned: 524 (million)
% 154.67/22.47 % (2110755)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2123348298:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2864 on theBenchmark for (2864ds/1016Mi)
% 176.54/25.54 % (2110755)Instruction limit reached!
% 176.54/25.54 % (2110755)------------------------------
% 176.54/25.54 % (2110755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.54/25.54 % (2110755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.54/25.54 % (2110755)CaDiCaL version: 2.1.3
% 176.54/25.54 % (2110755)Termination reason: Instruction limit
% 176.54/25.54 % (2110755)Termination phase: Saturation
% 176.54/25.54 % (2110755)Time elapsed: 0.471 s
% 176.54/25.54 % (2110755)Peak memory usage: 103 MB
% 176.54/25.54 % (2110755)Instructions burned: 1017 (million)
% 176.54/25.54 % (2111010)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3006658734:i=14123:bd=preordered:ins=4_2858 on theBenchmark for (2858ds/14123Mi)
% 176.54/25.54 % (2110464)Instruction limit reached!
% 176.54/25.54 % (2110464)------------------------------
% 176.54/25.54 % (2110464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.54/25.54 % (2110464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.54/25.54 % (2110464)CaDiCaL version: 2.1.3
% 176.54/25.54 % (2110464)Termination reason: Instruction limit
% 176.54/25.54 % (2110464)Termination phase: Saturation
% 176.54/25.54 % (2110464)Time elapsed: 4.070 s
% 176.54/25.54 % (2110464)Peak memory usage: 201 MB
% 176.54/25.54 % (2110464)Instructions burned: 11145 (million)
% 176.54/25.54 % (2111228)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2790371215:i=5781:kws=precedence:bd=all:rawr=on_2853 on theBenchmark for (2853ds/5781Mi)
% 176.54/25.54 % (2110458)Instruction limit reached!
% 176.54/25.54 % (2110458)------------------------------
% 176.54/25.54 % (2110458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.54/25.54 % (2110458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.54/25.54 % (2110458)CaDiCaL version: 2.1.3
% 176.54/25.54 % (2110458)Termination reason: Instruction limit
% 176.54/25.54 % (2110458)Termination phase: Saturation
% 176.54/25.54 % (2110458)Time elapsed: 5.835 s
% 176.54/25.54 % (2110458)Peak memory usage: 207 MB
% 176.54/25.54 % (2110458)Instructions burned: 9927 (million)
% 176.54/25.54 % (2111799)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2473494148:i=2448:gtgl=5:bd=preordered:gtg=all_2843 on theBenchmark for (2843ds/2448Mi)
% 176.54/25.54 % (2111228)Instruction limit reached!
% 176.54/25.54 % (2111228)------------------------------
% 176.54/25.54 % (2111228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.54/25.54 % (2111228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.54/25.54 % (2111228)CaDiCaL version: 2.1.3
% 176.54/25.54 % (2111228)Termination reason: Instruction limit
% 176.54/25.54 % (2111228)Termination phase: Saturation
% 176.54/25.54 % (2111228)Time elapsed: 1.976 s
% 176.54/25.54 % (2111228)Peak memory usage: 136 MB
% 176.54/25.54 % (2111228)Instructions burned: 5784 (million)
% 176.54/25.54 % (2112350)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2340429972:i=3223:kws=precedence:fgj=on:av=off_2832 on theBenchmark for (2832ds/3223Mi)
% 176.54/25.54 % (2111799)Instruction limit reached!
% 176.54/25.54 % (2111799)------------------------------
% 176.54/25.54 % (2111799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.54/25.54 % (2111799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.54/25.54 % (2111799)CaDiCaL version: 2.1.3
% 176.54/25.54 % (2111799)Termination reason: Instruction limit
% 176.54/25.54 % (2111799)Termination phase: Saturation
% 176.54/25.54 % (2111799)Time elapsed: 1.440 s
% 176.54/25.54 % (2111799)Peak memory usage: 145 MB
% 176.54/25.54 % (2111799)Instructions burned: 2448 (million)
% 176.54/25.54 % (2112658)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=126182240:st=5.6:i=2033:sd=3:ss=axioms_2827 on theBenchmark for (2827ds/2033Mi)
% 176.54/25.54 % (2112350)Instruction limit reached!
% 176.54/25.54 % (2112350)------------------------------
% 176.54/25.54 % (2112350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.54/25.54 % (2112350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.54/25.54 % (2112350)CaDiCaL version: 2.1.3
% 176.54/25.54 % (2112350)Termination reason: Instruction limit
% 176.54/25.54 % (2112350)Termination phase: Saturation
% 105.52/28.10 % (2112350)Time elapsed: 1.219 s
% 105.52/28.10 % (2112350)Peak memory usage: 148 MB
% 105.52/28.10 % (2112350)Instructions burned: 3225 (million)
% 105.52/28.10 % (2113073)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2151854712:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2819 on theBenchmark for (2819ds/2055Mi)
% 105.52/28.10 % (2110456)Instruction limit reached!
% 105.52/28.10 % (2110456)------------------------------
% 105.52/28.10 % (2110456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2110456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2110456)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2110456)Termination reason: Instruction limit
% 105.52/28.10 % (2110456)Termination phase: Saturation
% 105.52/28.10 % (2110456)Time elapsed: 8.487 s
% 105.52/28.10 % (2110456)Peak memory usage: 240 MB
% 105.52/28.10 % (2110456)Instructions burned: 13914 (million)
% 105.52/28.10 % (2113179)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=2713243354:i=21611:sd=3:ss=axioms_2817 on theBenchmark for (2817ds/21611Mi)
% 105.52/28.10 % (2112658)Instruction limit reached!
% 105.52/28.10 % (2112658)------------------------------
% 105.52/28.10 % (2112658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2112658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2112658)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2112658)Termination reason: Instruction limit
% 105.52/28.10 % (2112658)Termination phase: Saturation
% 105.52/28.10 % (2112658)Time elapsed: 1.341 s
% 105.52/28.10 % (2112658)Peak memory usage: 135 MB
% 105.52/28.10 % (2112658)Instructions burned: 2033 (million)
% 105.52/28.10 % (2113073)Instruction limit reached!
% 105.52/28.10 % (2113073)------------------------------
% 105.52/28.10 % (2113073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113073)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113073)Termination reason: Instruction limit
% 105.52/28.10 % (2113073)Termination phase: Saturation
% 105.52/28.10 % (2113073)Time elapsed: 0.732 s
% 105.52/28.10 % (2113073)Peak memory usage: 135 MB
% 105.52/28.10 % (2113073)Instructions burned: 2058 (million)
% 105.52/28.10 % (2113476)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3572544680:i=4835:sd=13:ss=axioms:sgt=23_2812 on theBenchmark for (2812ds/4835Mi)
% 105.52/28.10 % (2113532)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=721189356:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2811 on theBenchmark for (2811ds/797Mi)
% 105.52/28.10 % (2113532)Instruction limit reached!
% 105.52/28.10 % (2113532)------------------------------
% 105.52/28.10 % (2113532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113532)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113532)Termination reason: Instruction limit
% 105.52/28.10 % (2113532)Termination phase: Saturation
% 105.52/28.10 % (2113532)Time elapsed: 0.203 s
% 105.52/28.10 % (2113532)Peak memory usage: 91 MB
% 105.52/28.10 % (2113532)Instructions burned: 799 (million)
% 105.52/28.10 % (2113695)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1435213952:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2808 on theBenchmark for (2808ds/2326Mi)
% 105.52/28.10 % (2113695)Instruction limit reached!
% 105.52/28.10 % (2113695)------------------------------
% 105.52/28.10 % (2113695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113695)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113695)Termination reason: Instruction limit
% 105.52/28.10 % (2113695)Termination phase: Saturation
% 105.52/28.10 % (2113695)Time elapsed: 0.864 s
% 105.52/28.10 % (2113695)Peak memory usage: 114 MB
% 105.52/28.10 % (2113695)Instructions burned: 2326 (million)
% 105.52/28.10 % (2113840)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1682786569:i=6038:nm=6_2799 on theBenchmark for (2799ds/6038Mi)
% 105.52/28.10 % (2113476)Instruction limit reached!
% 105.52/28.10 % (2113476)------------------------------
% 105.52/28.10 % (2113476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113476)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113476)Termination reason: Instruction limit
% 105.52/28.10 % (2113476)Termination phase: Saturation
% 105.52/28.10 % (2113476)Time elapsed: 2.932 s
% 105.52/28.10 % (2113476)Peak memory usage: 129 MB
% 105.52/28.10 % (2113476)Instructions burned: 4835 (million)
% 105.52/28.10 % (2113842)lrs+10_1_sil=32000:sp=occurrence:random_seed=1792282757:st=2:i=33334:sd=3:ss=included:sgt=32_2781 on theBenchmark for (2781ds/33334Mi)
% 105.52/28.10 % (2113840)Instruction limit reached!
% 105.52/28.10 % (2113840)------------------------------
% 105.52/28.10 % (2113840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113840)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113840)Termination reason: Instruction limit
% 105.52/28.10 % (2113840)Termination phase: Saturation
% 105.52/28.10 % (2113840)Time elapsed: 1.856 s
% 105.52/28.10 % (2113840)Peak memory usage: 174 MB
% 105.52/28.10 % (2113840)Instructions burned: 6041 (million)
% 105.52/28.10 % (2113844)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=66039406:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2779 on theBenchmark for (2779ds/1008Mi)
% 105.52/28.10 % (2113844)Instruction limit reached!
% 105.52/28.10 % (2113844)------------------------------
% 105.52/28.10 % (2113844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113844)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113844)Termination reason: Instruction limit
% 105.52/28.10 % (2113844)Termination phase: Saturation
% 105.52/28.10 % (2113844)Time elapsed: 0.271 s
% 105.52/28.10 % (2113844)Peak memory usage: 103 MB
% 105.52/28.10 % (2113844)Instructions burned: 1011 (million)
% 105.52/28.10 % (2113846)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=2799998461:i=8327:s2at=5:bd=preordered_2775 on theBenchmark for (2775ds/8327Mi)
% 105.52/28.10 % (2111010)Instruction limit reached!
% 105.52/28.10 % (2111010)------------------------------
% 105.52/28.10 % (2111010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2111010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2111010)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2111010)Termination reason: Instruction limit
% 105.52/28.10 % (2111010)Termination phase: Saturation
% 105.52/28.10 % (2111010)Time elapsed: 8.292 s
% 105.52/28.10 % (2111010)Peak memory usage: 230 MB
% 105.52/28.10 % (2111010)Instructions burned: 14124 (million)
% 105.52/28.10 % (2113848)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3282567313:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2773 on theBenchmark for (2773ds/1083Mi)
% 105.52/28.10 % (2113848)Instruction limit reached!
% 105.52/28.10 % (2113848)------------------------------
% 105.52/28.10 % (2113848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113848)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113848)Termination reason: Instruction limit
% 105.52/28.10 % (2113848)Termination phase: Saturation
% 105.52/28.10 % (2113848)Time elapsed: 0.630 s
% 105.52/28.10 % (2113848)Peak memory usage: 104 MB
% 105.52/28.10 % (2113848)Instructions burned: 1084 (million)
% 105.52/28.10 % (2113870)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2966840553:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2765 on theBenchmark for (2765ds/1084Mi)
% 105.52/28.10 % (2113870)Instruction limit reached!
% 105.52/28.10 % (2113870)------------------------------
% 105.52/28.10 % (2113870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113870)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113870)Termination reason: Instruction limit
% 105.52/28.10 % (2113870)Termination phase: Saturation
% 105.52/28.10 % (2113870)Time elapsed: 1.007 s
% 105.52/28.10 % (2113870)Peak memory usage: 100 MB
% 105.52/28.10 % (2113870)Instructions burned: 1084 (million)
% 105.52/28.10 % (2113884)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3419864770:i=6995:s2at=5:gtg=all_2753 on theBenchmark for (2753ds/6995Mi)
% 105.52/28.10 % (2113846)Instruction limit reached!
% 105.52/28.10 % (2113846)------------------------------
% 105.52/28.10 % (2113846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.52/28.10 % (2113846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.52/28.10 % (2113846)CaDiCaL version: 2.1.3
% 105.52/28.10 % (2113846)Termination reason: Instruction limit
% 105.52/28.10 % (2113846)Termination phase: Saturation
% 105.52/28.10 % (2113846)Time elapsed: 4.379 s
% 105.52/28.10 % (2113846)Peak memory usage: 188 MB
% 105.52/28.10 % (2113846)Instructions burned: 8329 (million)
% 105.52/28.10 % (2113884)First to succeed.
% 105.52/28.10 % (2113884)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2110223"
% 105.52/28.10 % (2113898)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3816240413:st=2:i=6225:sd=15:ss=axioms_2731 on theBenchmark for (2731ds/6225Mi)
% 105.52/28.10 % (2113884)Refutation found. Thanks to Tanya!
% 105.52/28.10 % SZS status Theorem for theBenchmark
% 105.52/28.10 % SZS output start Proof for theBenchmark
% See solution above
% 194.99/28.25 % (2113884)------------------------------
% 194.99/28.25 % (2113884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.99/28.25 % (2113884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.99/28.25 % (2113884)CaDiCaL version: 2.1.3
% 194.99/28.25 % (2113884)Termination reason: Refutation
% 194.99/28.25 % (2113884)Time elapsed: 2.067 s
% 194.99/28.25 % (2113884)Peak memory usage: 138 MB
% 194.99/28.25 % (2113884)Instructions burned: 1906 (million)
% 194.99/28.25 % (2113884)------------------------------
% 194.99/28.25 % (2113884)------------------------------
% 194.99/28.25 % (2110223)Success in time 27.428 s
% 194.99/28.25 % Vampire exiting
%------------------------------------------------------------------------------