%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU448+4 : 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 : n015.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 12:49:10 PM UTC 2026
% Result : Theorem 123.41s 36.26s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 48
% Syntax : Number of formulae : 280 ( 59 unt; 35 def)
% Number of atoms : 936 ( 51 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1239 ( 583 ~; 576 |; 19 &)
% ( 37 <=>; 23 =>; 0 <=; 1 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 29 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 12 con; 0-4 aty)
% Number of variables : 235 ( 0 sgn 220 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f514,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ( r1_tarski(X1,X2)
<=> r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_subset_1) ).
fof(f518,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ( r1_tarski(X1,k3_subset_1(X0,X2))
=> r1_tarski(X2,k3_subset_1(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_subset_1) ).
fof(f526,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ( r1_xboole_0(X1,X2)
<=> r1_tarski(X1,k3_subset_1(X0,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t43_subset_1) ).
fof(f565,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f566,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> k3_subset_1(X0,k3_subset_1(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
fof(f1481,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1498,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_relset_1) ).
fof(f1500,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_relset_1) ).
fof(f1507,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_relset_1) ).
fof(f1508,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f71128,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( r1_xboole_0(X2,k9_relat_1(k4_relat_1(X4),X3))
<=> r1_xboole_0(X3,k9_relat_1(X4,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_relset_2) ).
fof(f71144,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ( r1_tarski(k10_relset_1(X0,X1,X4,k3_subset_1(X0,X2)),k3_subset_1(X1,X3))
<=> r1_tarski(k10_relset_1(X1,X0,k6_relset_1(X0,X1,X4),X3),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t62_relset_2) ).
fof(f71145,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ( r1_tarski(k10_relset_1(X0,X1,X4,k3_subset_1(X0,X2)),k3_subset_1(X1,X3))
<=> r1_tarski(k10_relset_1(X1,X0,k6_relset_1(X0,X1,X4),X3),X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f71144]) ).
fof(f71257,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( ( r1_tarski(k10_relset_1(X0,X1,X4,k3_subset_1(X0,X2)),k3_subset_1(X1,X3))
<~> r1_tarski(k10_relset_1(X1,X0,k6_relset_1(X0,X1,X4),X3),X2) )
& m2_relset_1(X4,X0,X1) )
& m1_subset_1(X3,k1_zfmisc_1(X1)) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71145]) ).
fof(f71322,plain,
! [X0,X1] :
( k3_subset_1(X0,k3_subset_1(X0,X1)) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f566]) ).
fof(f71323,plain,
! [X0,X1] :
( m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f565]) ).
fof(f71339,plain,
! [X0,X1] :
( ! [X2] :
( ( r1_xboole_0(X1,X2)
<=> r1_tarski(X1,k3_subset_1(X0,X2)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f526]) ).
fof(f71346,plain,
! [X0,X1] :
( ! [X2] :
( r1_tarski(X2,k3_subset_1(X0,X1))
| ~ r1_tarski(X1,k3_subset_1(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f518]) ).
fof(f71347,plain,
! [X0,X1] :
( ! [X2] :
( r1_tarski(X2,k3_subset_1(X0,X1))
| ~ r1_tarski(X1,k3_subset_1(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f71346]) ).
fof(f71348,plain,
! [X0,X1] :
( ! [X2] :
( ( r1_tarski(X1,X2)
<=> r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f514]) ).
fof(f71358,plain,
! [X0,X1,X2] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1500]) ).
fof(f71360,plain,
! [X0,X1,X2] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1498]) ).
fof(f71368,plain,
! [X0,X1,X2,X3] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1508]) ).
fof(f71369,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1507]) ).
fof(f71903,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1481]) ).
fof(f71912,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( ( r1_xboole_0(X2,k9_relat_1(k4_relat_1(X4),X3))
<=> r1_xboole_0(X3,k9_relat_1(X4,X2)) )
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71128]) ).
fof(f76570,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( ( ~ r1_tarski(k10_relset_1(X1,X0,k6_relset_1(X0,X1,X4),X3),X2)
| ~ r1_tarski(k10_relset_1(X0,X1,X4,k3_subset_1(X0,X2)),k3_subset_1(X1,X3)) )
& ( r1_tarski(k10_relset_1(X1,X0,k6_relset_1(X0,X1,X4),X3),X2)
| r1_tarski(k10_relset_1(X0,X1,X4,k3_subset_1(X0,X2)),k3_subset_1(X1,X3)) )
& m2_relset_1(X4,X0,X1) )
& m1_subset_1(X3,k1_zfmisc_1(X1)) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f71257]) ).
fof(f76571,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( ( ~ r1_tarski(k10_relset_1(X1,X0,k6_relset_1(X0,X1,X4),X3),X2)
| ~ r1_tarski(k10_relset_1(X0,X1,X4,k3_subset_1(X0,X2)),k3_subset_1(X1,X3)) )
& ( r1_tarski(k10_relset_1(X1,X0,k6_relset_1(X0,X1,X4),X3),X2)
| r1_tarski(k10_relset_1(X0,X1,X4,k3_subset_1(X0,X2)),k3_subset_1(X1,X3)) )
& m2_relset_1(X4,X0,X1) )
& m1_subset_1(X3,k1_zfmisc_1(X1)) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f76570]) ).
fof(f76572,plain,
( ( ~ r1_tarski(k10_relset_1(sK73,sK72,k6_relset_1(sK72,sK73,sK76),sK75),sK74)
| ~ r1_tarski(k10_relset_1(sK72,sK73,sK76,k3_subset_1(sK72,sK74)),k3_subset_1(sK73,sK75)) )
& ( r1_tarski(k10_relset_1(sK73,sK72,k6_relset_1(sK72,sK73,sK76),sK75),sK74)
| r1_tarski(k10_relset_1(sK72,sK73,sK76,k3_subset_1(sK72,sK74)),k3_subset_1(sK73,sK75)) )
& m2_relset_1(sK76,sK72,sK73)
& m1_subset_1(sK75,k1_zfmisc_1(sK73))
& m1_subset_1(sK74,k1_zfmisc_1(sK72)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72,sK73,sK74,sK75,sK76]),skolemize(X0,sK72),skolemize(X1,sK73),skolemize(X2,sK74),skolemize(X3,sK75),skolemize(X4,sK76)],[f76571]) ).
fof(f76607,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r1_xboole_0(X1,X2)
| ~ r1_tarski(X1,k3_subset_1(X0,X2)) )
& ( r1_tarski(X1,k3_subset_1(X0,X2))
| ~ r1_xboole_0(X1,X2) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f71339]) ).
fof(f76608,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r1_tarski(X1,X2)
| ~ r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1)) )
& ( r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1))
| ~ r1_tarski(X1,X2) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f71348]) ).
fof(f76870,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( ( ( r1_xboole_0(X2,k9_relat_1(k4_relat_1(X4),X3))
| ~ r1_xboole_0(X3,k9_relat_1(X4,X2)) )
& ( r1_xboole_0(X3,k9_relat_1(X4,X2))
| ~ r1_xboole_0(X2,k9_relat_1(k4_relat_1(X4),X3)) ) )
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f71912]) ).
fof(f76931,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1483]) ).
fof(f77978,plain,
m1_subset_1(sK74,k1_zfmisc_1(sK72)),
inference(cnf_transformation,[],[f76572]) ).
fof(f77979,plain,
m1_subset_1(sK75,k1_zfmisc_1(sK73)),
inference(cnf_transformation,[],[f76572]) ).
fof(f77980,plain,
m2_relset_1(sK76,sK72,sK73),
inference(cnf_transformation,[],[f76572]) ).
fof(f77981,plain,
( r1_tarski(k10_relset_1(sK73,sK72,k6_relset_1(sK72,sK73,sK76),sK75),sK74)
| r1_tarski(k10_relset_1(sK72,sK73,sK76,k3_subset_1(sK72,sK74)),k3_subset_1(sK73,sK75)) ),
inference(cnf_transformation,[],[f76572]) ).
fof(f77982,plain,
( ~ r1_tarski(k10_relset_1(sK73,sK72,k6_relset_1(sK72,sK73,sK76),sK75),sK74)
| ~ r1_tarski(k10_relset_1(sK72,sK73,sK76,k3_subset_1(sK72,sK74)),k3_subset_1(sK73,sK75)) ),
inference(cnf_transformation,[],[f76572]) ).
fof(f78058,plain,
! [X0,X1] :
( k3_subset_1(X0,k3_subset_1(X0,X1)) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f71322]) ).
fof(f78059,plain,
! [X0,X1] :
( m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f71323]) ).
fof(f78075,plain,
! [X2,X0,X1] :
( r1_tarski(X1,k3_subset_1(X0,X2))
| ~ r1_xboole_0(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f76607]) ).
fof(f78076,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X1,k3_subset_1(X0,X2))
| r1_xboole_0(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f76607]) ).
fof(f78081,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X1,k3_subset_1(X0,X2))
| r1_tarski(X2,k3_subset_1(X0,X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f71347]) ).
fof(f78082,plain,
! [X2,X0,X1] :
( r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1))
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f76608]) ).
fof(f78083,plain,
! [X2,X0,X1] :
( ~ r1_tarski(k3_subset_1(X0,X2),k3_subset_1(X0,X1))
| r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f76608]) ).
fof(f78097,plain,
! [X2,X0,X1] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71358]) ).
fof(f78099,plain,
! [X2,X0,X1] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71360]) ).
fof(f78117,plain,
! [X2,X3,X0,X1] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71368]) ).
fof(f78118,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71369]) ).
fof(f79013,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71903]) ).
fof(f79023,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ r1_xboole_0(X2,k9_relat_1(k4_relat_1(X4),X3))
| r1_xboole_0(X3,k9_relat_1(X4,X2))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f76870]) ).
fof(f79024,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ r1_xboole_0(X3,k9_relat_1(X4,X2))
| r1_xboole_0(X2,k9_relat_1(k4_relat_1(X4),X3))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f76870]) ).
fof(f79370,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f76931]) ).
fof(f85577,definition,
sF943 = k6_relset_1(sK72,sK73,sK76),
introduced(definition,[new_symbols(definition,[sF943])],[function_definition]) ).
fof(f85578,plain,
k6_relset_1(sK72,sK73,sK76) = sF943,
inference(reorient_equations,[],[f85577]) ).
fof(f85579,definition,
sF944 = k10_relset_1(sK73,sK72,sF943,sK75),
introduced(definition,[new_symbols(definition,[sF944])],[function_definition]) ).
fof(f85580,plain,
k10_relset_1(sK73,sK72,sF943,sK75) = sF944,
inference(reorient_equations,[],[f85579]) ).
fof(f85581,definition,
sF945 = k3_subset_1(sK72,sK74),
introduced(definition,[new_symbols(definition,[sF945])],[function_definition]) ).
fof(f85582,plain,
k3_subset_1(sK72,sK74) = sF945,
inference(reorient_equations,[],[f85581]) ).
fof(f85583,definition,
sF946 = k10_relset_1(sK72,sK73,sK76,sF945),
introduced(definition,[new_symbols(definition,[sF946])],[function_definition]) ).
fof(f85584,plain,
k10_relset_1(sK72,sK73,sK76,sF945) = sF946,
inference(reorient_equations,[],[f85583]) ).
fof(f85585,definition,
sF947 = k3_subset_1(sK73,sK75),
introduced(definition,[new_symbols(definition,[sF947])],[function_definition]) ).
fof(f85586,plain,
k3_subset_1(sK73,sK75) = sF947,
inference(reorient_equations,[],[f85585]) ).
fof(f85587,plain,
( ~ r1_tarski(sF944,sK74)
| ~ r1_tarski(sF946,sF947) ),
inference(definition_folding,[],[f77982,f85586,f85584,f85582,f85580,f85578]) ).
fof(f85588,plain,
( r1_tarski(sF944,sK74)
| r1_tarski(sF946,sF947) ),
inference(definition_folding,[],[f77981,f85586,f85584,f85582,f85580,f85578]) ).
fof(f85589,definition,
sF948 = k1_zfmisc_1(sK73),
introduced(definition,[new_symbols(definition,[sF948])],[function_definition]) ).
fof(f85590,plain,
k1_zfmisc_1(sK73) = sF948,
inference(reorient_equations,[],[f85589]) ).
fof(f85591,plain,
m1_subset_1(sK75,sF948),
inference(definition_folding,[],[f77979,f85590]) ).
fof(f85592,definition,
sF949 = k1_zfmisc_1(sK72),
introduced(definition,[new_symbols(definition,[sF949])],[function_definition]) ).
fof(f85593,plain,
k1_zfmisc_1(sK72) = sF949,
inference(reorient_equations,[],[f85592]) ).
fof(f85594,plain,
m1_subset_1(sK74,sF949),
inference(definition_folding,[],[f77978,f85593]) ).
fof(f88186,definition,
( spl950_514
<=> m1_subset_1(sK74,sF949) ),
introduced(definition,[new_symbols(definition,[spl950_514])],[avatar_definition]) ).
fof(f88188,plain,
( m1_subset_1(sK74,sF949)
| ~ spl950_514 ),
inference(avatar_component_clause,[],[f88186]) ).
fof(f88189,plain,
spl950_514,
inference(avatar_split_clause,[],[f85594,f88186]) ).
fof(f88191,definition,
( spl950_515
<=> m1_subset_1(sK75,sF948) ),
introduced(definition,[new_symbols(definition,[spl950_515])],[avatar_definition]) ).
fof(f88193,plain,
( m1_subset_1(sK75,sF948)
| ~ spl950_515 ),
inference(avatar_component_clause,[],[f88191]) ).
fof(f88194,plain,
spl950_515,
inference(avatar_split_clause,[],[f85591,f88191]) ).
fof(f88196,definition,
( spl950_516
<=> m2_relset_1(sK76,sK72,sK73) ),
introduced(definition,[new_symbols(definition,[spl950_516])],[avatar_definition]) ).
fof(f88198,plain,
( m2_relset_1(sK76,sK72,sK73)
| ~ spl950_516 ),
inference(avatar_component_clause,[],[f88196]) ).
fof(f88199,plain,
spl950_516,
inference(avatar_split_clause,[],[f77980,f88196]) ).
fof(f88201,definition,
( spl950_517
<=> r1_tarski(sF946,sF947) ),
introduced(definition,[new_symbols(definition,[spl950_517])],[avatar_definition]) ).
fof(f88205,definition,
( spl950_518
<=> r1_tarski(sF944,sK74) ),
introduced(definition,[new_symbols(definition,[spl950_518])],[avatar_definition]) ).
fof(f88207,plain,
( r1_tarski(sF944,sK74)
| ~ spl950_518 ),
inference(avatar_component_clause,[],[f88205]) ).
fof(f88208,plain,
( spl950_517
| spl950_518 ),
inference(avatar_split_clause,[],[f85588,f88205,f88201]) ).
fof(f88209,plain,
( ~ spl950_517
| ~ spl950_518 ),
inference(avatar_split_clause,[],[f85587,f88205,f88201]) ).
fof(f88216,definition,
( spl950_520
<=> k6_relset_1(sK72,sK73,sK76) = sF943 ),
introduced(definition,[new_symbols(definition,[spl950_520])],[avatar_definition]) ).
fof(f88218,plain,
( k6_relset_1(sK72,sK73,sK76) = sF943
| ~ spl950_520 ),
inference(avatar_component_clause,[],[f88216]) ).
fof(f88219,plain,
spl950_520,
inference(avatar_split_clause,[],[f85578,f88216]) ).
fof(f88221,definition,
( spl950_521
<=> k10_relset_1(sK73,sK72,sF943,sK75) = sF944 ),
introduced(definition,[new_symbols(definition,[spl950_521])],[avatar_definition]) ).
fof(f88223,plain,
( k10_relset_1(sK73,sK72,sF943,sK75) = sF944
| ~ spl950_521 ),
inference(avatar_component_clause,[],[f88221]) ).
fof(f88224,plain,
spl950_521,
inference(avatar_split_clause,[],[f85580,f88221]) ).
fof(f88226,definition,
( spl950_522
<=> k3_subset_1(sK72,sK74) = sF945 ),
introduced(definition,[new_symbols(definition,[spl950_522])],[avatar_definition]) ).
fof(f88228,plain,
( k3_subset_1(sK72,sK74) = sF945
| ~ spl950_522 ),
inference(avatar_component_clause,[],[f88226]) ).
fof(f88229,plain,
spl950_522,
inference(avatar_split_clause,[],[f85582,f88226]) ).
fof(f88231,definition,
( spl950_523
<=> k10_relset_1(sK72,sK73,sK76,sF945) = sF946 ),
introduced(definition,[new_symbols(definition,[spl950_523])],[avatar_definition]) ).
fof(f88233,plain,
( k10_relset_1(sK72,sK73,sK76,sF945) = sF946
| ~ spl950_523 ),
inference(avatar_component_clause,[],[f88231]) ).
fof(f88234,plain,
spl950_523,
inference(avatar_split_clause,[],[f85584,f88231]) ).
fof(f88236,definition,
( spl950_524
<=> k3_subset_1(sK73,sK75) = sF947 ),
introduced(definition,[new_symbols(definition,[spl950_524])],[avatar_definition]) ).
fof(f88238,plain,
( k3_subset_1(sK73,sK75) = sF947
| ~ spl950_524 ),
inference(avatar_component_clause,[],[f88236]) ).
fof(f88239,plain,
spl950_524,
inference(avatar_split_clause,[],[f85586,f88236]) ).
fof(f88241,definition,
( spl950_525
<=> k1_zfmisc_1(sK73) = sF948 ),
introduced(definition,[new_symbols(definition,[spl950_525])],[avatar_definition]) ).
fof(f88243,plain,
( k1_zfmisc_1(sK73) = sF948
| ~ spl950_525 ),
inference(avatar_component_clause,[],[f88241]) ).
fof(f88244,plain,
spl950_525,
inference(avatar_split_clause,[],[f85590,f88241]) ).
fof(f88246,definition,
( spl950_526
<=> k1_zfmisc_1(sK72) = sF949 ),
introduced(definition,[new_symbols(definition,[spl950_526])],[avatar_definition]) ).
fof(f88248,plain,
( k1_zfmisc_1(sK72) = sF949
| ~ spl950_526 ),
inference(avatar_component_clause,[],[f88246]) ).
fof(f88249,plain,
spl950_526,
inference(avatar_split_clause,[],[f85593,f88246]) ).
fof(f88251,plain,
( m1_subset_1(sF944,k1_zfmisc_1(sK72))
| ~ m1_relset_1(sF943,sK73,sK72)
| ~ spl950_521 ),
inference(superposition,[],[f78118,f88223]) ).
fof(f88252,plain,
( m1_subset_1(sF946,k1_zfmisc_1(sK73))
| ~ m1_relset_1(sK76,sK72,sK73)
| ~ spl950_523 ),
inference(superposition,[],[f78118,f88233]) ).
fof(f88255,plain,
( m1_subset_1(sF946,sF948)
| ~ m1_relset_1(sK76,sK72,sK73)
| ~ spl950_523
| ~ spl950_525 ),
inference(forward_demodulation,[],[f88252,f88243]) ).
fof(f88256,plain,
( m1_subset_1(sF944,sF949)
| ~ m1_relset_1(sF943,sK73,sK72)
| ~ spl950_521
| ~ spl950_526 ),
inference(forward_demodulation,[],[f88251,f88248]) ).
fof(f88258,definition,
( spl950_527
<=> m1_relset_1(sK76,sK72,sK73) ),
introduced(definition,[new_symbols(definition,[spl950_527])],[avatar_definition]) ).
fof(f88262,definition,
( spl950_528
<=> m1_subset_1(sF946,sF948) ),
introduced(definition,[new_symbols(definition,[spl950_528])],[avatar_definition]) ).
fof(f88264,plain,
( m1_subset_1(sF946,sF948)
| ~ spl950_528 ),
inference(avatar_component_clause,[],[f88262]) ).
fof(f88265,plain,
( ~ spl950_527
| spl950_528
| ~ spl950_523
| ~ spl950_525 ),
inference(avatar_split_clause,[],[f88255,f88241,f88231,f88262,f88258]) ).
fof(f88267,definition,
( spl950_529
<=> m1_relset_1(sF943,sK73,sK72) ),
introduced(definition,[new_symbols(definition,[spl950_529])],[avatar_definition]) ).
fof(f88271,definition,
( spl950_530
<=> m1_subset_1(sF944,sF949) ),
introduced(definition,[new_symbols(definition,[spl950_530])],[avatar_definition]) ).
fof(f88273,plain,
( m1_subset_1(sF944,sF949)
| ~ spl950_530 ),
inference(avatar_component_clause,[],[f88271]) ).
fof(f88274,plain,
( ~ spl950_529
| spl950_530
| ~ spl950_521
| ~ spl950_526 ),
inference(avatar_split_clause,[],[f88256,f88246,f88221,f88271,f88267]) ).
fof(f88288,plain,
( ! [X0] :
( ~ r1_tarski(sF945,k3_subset_1(sK72,X0))
| r1_tarski(X0,sK74)
| ~ m1_subset_1(sK74,k1_zfmisc_1(sK72))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK72)) )
| ~ spl950_522 ),
inference(superposition,[],[f78083,f88228]) ).
fof(f88295,plain,
( ! [X0] :
( ~ m1_subset_1(sK74,sF949)
| ~ r1_tarski(sF945,k3_subset_1(sK72,X0))
| r1_tarski(X0,sK74)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK72)) )
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_demodulation,[],[f88288,f88248]) ).
fof(f88299,plain,
( ! [X0] :
( ~ r1_tarski(sF945,k3_subset_1(sK72,X0))
| r1_tarski(X0,sK74)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK72)) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_subsumption_resolution,[],[f88295,f88188]) ).
fof(f88303,plain,
( ! [X0] :
( ~ r1_tarski(sF945,k3_subset_1(sK72,X0))
| ~ m1_subset_1(X0,sF949)
| r1_tarski(X0,sK74) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_demodulation,[],[f88299,f88248]) ).
fof(f88308,plain,
( ! [X0] :
( ~ r1_tarski(X0,sF947)
| r1_tarski(sK75,k3_subset_1(sK73,X0))
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK73)) )
| ~ spl950_524 ),
inference(superposition,[],[f78081,f88238]) ).
fof(f88312,plain,
( ! [X0] :
( ~ m1_subset_1(sK75,sF948)
| ~ r1_tarski(X0,sF947)
| r1_tarski(sK75,k3_subset_1(sK73,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK73)) )
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_demodulation,[],[f88308,f88243]) ).
fof(f88314,plain,
( ! [X0] :
( ~ r1_tarski(X0,sF947)
| r1_tarski(sK75,k3_subset_1(sK73,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK73)) )
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_subsumption_resolution,[],[f88312,f88193]) ).
fof(f88316,plain,
( ! [X0] :
( r1_tarski(sK75,k3_subset_1(sK73,X0))
| ~ r1_tarski(X0,sF947)
| ~ m1_subset_1(X0,sF948) )
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_demodulation,[],[f88314,f88243]) ).
fof(f88325,plain,
( sF943 = k4_relat_1(sK76)
| ~ m1_relset_1(sK76,sK72,sK73)
| ~ spl950_520 ),
inference(superposition,[],[f78097,f88218]) ).
fof(f88329,definition,
( spl950_532
<=> sF943 = k4_relat_1(sK76) ),
introduced(definition,[new_symbols(definition,[spl950_532])],[avatar_definition]) ).
fof(f88331,plain,
( sF943 = k4_relat_1(sK76)
| ~ spl950_532 ),
inference(avatar_component_clause,[],[f88329]) ).
fof(f88333,plain,
( ~ spl950_527
| spl950_532
| ~ spl950_520 ),
inference(avatar_split_clause,[],[f88325,f88216,f88329,f88258]) ).
fof(f88337,plain,
( sK75 = k3_subset_1(sK73,sF947)
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ spl950_524 ),
inference(superposition,[],[f78058,f88238]) ).
fof(f88348,plain,
( ~ m1_subset_1(sK75,sF948)
| sK75 = k3_subset_1(sK73,sF947)
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_demodulation,[],[f88337,f88243]) ).
fof(f88350,plain,
( sK75 = k3_subset_1(sK73,sF947)
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_subsumption_resolution,[],[f88348,f88193]) ).
fof(f88357,definition,
( spl950_534
<=> sK75 = k3_subset_1(sK73,sF947) ),
introduced(definition,[new_symbols(definition,[spl950_534])],[avatar_definition]) ).
fof(f88359,plain,
( sK75 = k3_subset_1(sK73,sF947)
| ~ spl950_534 ),
inference(avatar_component_clause,[],[f88357]) ).
fof(f88360,plain,
( spl950_534
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(avatar_split_clause,[],[f88350,f88241,f88236,f88191,f88357]) ).
fof(f88361,plain,
( m2_relset_1(sF943,sK73,sK72)
| ~ m1_relset_1(sK76,sK72,sK73)
| ~ spl950_520 ),
inference(superposition,[],[f78099,f88218]) ).
fof(f88365,definition,
( spl950_535
<=> m2_relset_1(sF943,sK73,sK72) ),
introduced(definition,[new_symbols(definition,[spl950_535])],[avatar_definition]) ).
fof(f88367,plain,
( m2_relset_1(sF943,sK73,sK72)
| ~ spl950_535 ),
inference(avatar_component_clause,[],[f88365]) ).
fof(f88368,plain,
( ~ spl950_527
| spl950_535
| ~ spl950_520 ),
inference(avatar_split_clause,[],[f88361,f88216,f88365,f88258]) ).
fof(f88372,plain,
( ! [X0] :
( r1_tarski(sF945,k3_subset_1(sK72,X0))
| ~ r1_tarski(X0,sK74)
| ~ m1_subset_1(sK74,k1_zfmisc_1(sK72))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK72)) )
| ~ spl950_522 ),
inference(superposition,[],[f78082,f88228]) ).
fof(f88381,plain,
( ! [X0] :
( ~ m1_subset_1(sK74,sF949)
| r1_tarski(sF945,k3_subset_1(sK72,X0))
| ~ r1_tarski(X0,sK74)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK72)) )
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_demodulation,[],[f88372,f88248]) ).
fof(f88385,plain,
( ! [X0] :
( r1_tarski(sF945,k3_subset_1(sK72,X0))
| ~ r1_tarski(X0,sK74)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK72)) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_subsumption_resolution,[],[f88381,f88188]) ).
fof(f88389,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF949)
| r1_tarski(sF945,k3_subset_1(sK72,X0))
| ~ r1_tarski(X0,sK74) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_demodulation,[],[f88385,f88248]) ).
fof(f88405,definition,
( spl950_537
<=> m1_subset_1(sF947,sF948) ),
introduced(definition,[new_symbols(definition,[spl950_537])],[avatar_definition]) ).
fof(f88430,definition,
( spl950_538
<=> m1_subset_1(sF945,sF949) ),
introduced(definition,[new_symbols(definition,[spl950_538])],[avatar_definition]) ).
fof(f88431,plain,
( m1_subset_1(sF945,sF949)
| ~ spl950_538 ),
inference(avatar_component_clause,[],[f88430]) ).
fof(f88450,definition,
( spl950_543
<=> ! [X0] :
( ~ m1_subset_1(X0,sF949)
| r1_tarski(sF945,k3_subset_1(sK72,X0))
| ~ r1_tarski(X0,sK74) ) ),
introduced(definition,[new_symbols(definition,[spl950_543])],[avatar_definition]) ).
fof(f88451,plain,
( ! [X0] :
( r1_tarski(sF945,k3_subset_1(sK72,X0))
| ~ m1_subset_1(X0,sF949)
| ~ r1_tarski(X0,sK74) )
| ~ spl950_543 ),
inference(avatar_component_clause,[],[f88450]) ).
fof(f88461,plain,
( sF944 = k9_relat_1(sF943,sK75)
| ~ m1_relset_1(sF943,sK73,sK72)
| ~ spl950_521 ),
inference(superposition,[],[f78117,f88223]) ).
fof(f88462,plain,
( sF946 = k9_relat_1(sK76,sF945)
| ~ m1_relset_1(sK76,sK72,sK73)
| ~ spl950_523 ),
inference(superposition,[],[f78117,f88233]) ).
fof(f88472,definition,
( spl950_545
<=> sF946 = k9_relat_1(sK76,sF945) ),
introduced(definition,[new_symbols(definition,[spl950_545])],[avatar_definition]) ).
fof(f88474,plain,
( sF946 = k9_relat_1(sK76,sF945)
| ~ spl950_545 ),
inference(avatar_component_clause,[],[f88472]) ).
fof(f88477,definition,
( spl950_546
<=> sF944 = k9_relat_1(sF943,sK75) ),
introduced(definition,[new_symbols(definition,[spl950_546])],[avatar_definition]) ).
fof(f88479,plain,
( sF944 = k9_relat_1(sF943,sK75)
| ~ spl950_546 ),
inference(avatar_component_clause,[],[f88477]) ).
fof(f88481,plain,
( ~ spl950_527
| spl950_545
| ~ spl950_523 ),
inference(avatar_split_clause,[],[f88462,f88231,f88472,f88258]) ).
fof(f88482,plain,
( ~ spl950_529
| spl950_546
| ~ spl950_521 ),
inference(avatar_split_clause,[],[f88461,f88221,f88477,f88267]) ).
fof(f88483,plain,
( spl950_543
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(avatar_split_clause,[],[f88389,f88246,f88226,f88186,f88450]) ).
fof(f88484,plain,
( m1_subset_1(sF947,k1_zfmisc_1(sK73))
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ spl950_524 ),
inference(superposition,[],[f78059,f88238]) ).
fof(f88485,plain,
( m1_subset_1(sF945,k1_zfmisc_1(sK72))
| ~ m1_subset_1(sK74,k1_zfmisc_1(sK72))
| ~ spl950_522 ),
inference(superposition,[],[f78059,f88228]) ).
fof(f88491,plain,
( m1_subset_1(sF945,sF949)
| ~ m1_subset_1(sK74,k1_zfmisc_1(sK72))
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_demodulation,[],[f88485,f88248]) ).
fof(f88492,plain,
( m1_subset_1(sF947,sF948)
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_demodulation,[],[f88484,f88243]) ).
fof(f88493,plain,
( ~ m1_subset_1(sK74,sF949)
| m1_subset_1(sF945,sF949)
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_demodulation,[],[f88491,f88248]) ).
fof(f88494,plain,
( ~ m1_subset_1(sK75,sF948)
| m1_subset_1(sF947,sF948)
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_demodulation,[],[f88492,f88243]) ).
fof(f88495,plain,
( m1_subset_1(sF945,sF949)
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_subsumption_resolution,[],[f88493,f88188]) ).
fof(f88496,plain,
( m1_subset_1(sF947,sF948)
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_subsumption_resolution,[],[f88494,f88193]) ).
fof(f88497,plain,
( spl950_538
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(avatar_split_clause,[],[f88495,f88246,f88226,f88186,f88430]) ).
fof(f88498,plain,
( spl950_537
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(avatar_split_clause,[],[f88496,f88241,f88236,f88191,f88405]) ).
fof(f88576,plain,
( m1_relset_1(sK76,sK72,sK73)
| ~ spl950_516 ),
inference(resolution,[],[f79370,f88198]) ).
fof(f88578,plain,
( spl950_527
| ~ spl950_516 ),
inference(avatar_split_clause,[],[f88576,f88196,f88258]) ).
fof(f88593,plain,
( m1_relset_1(sF943,sK73,sK72)
| ~ spl950_535 ),
inference(resolution,[],[f88367,f79370]) ).
fof(f88594,plain,
( spl950_529
| ~ spl950_535 ),
inference(avatar_split_clause,[],[f88593,f88365,f88267]) ).
fof(f88676,plain,
( ! [X0] :
( ~ r1_tarski(sK75,k3_subset_1(sK73,X0))
| r1_tarski(X0,sF947)
| ~ m1_subset_1(sF947,k1_zfmisc_1(sK73))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK73)) )
| ~ spl950_534 ),
inference(superposition,[],[f78083,f88359]) ).
fof(f88679,plain,
( ! [X0] :
( ~ m1_subset_1(sF947,sF948)
| ~ r1_tarski(sK75,k3_subset_1(sK73,X0))
| r1_tarski(X0,sF947)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK73)) )
| ~ spl950_525
| ~ spl950_534 ),
inference(forward_demodulation,[],[f88676,f88243]) ).
fof(f88692,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF948)
| ~ m1_subset_1(sF947,sF948)
| ~ r1_tarski(sK75,k3_subset_1(sK73,X0))
| r1_tarski(X0,sF947) )
| ~ spl950_525
| ~ spl950_534 ),
inference(forward_demodulation,[],[f88679,f88243]) ).
fof(f88700,definition,
( spl950_566
<=> ! [X0] :
( ~ m1_subset_1(X0,sF948)
| r1_tarski(X0,sF947)
| ~ r1_tarski(sK75,k3_subset_1(sK73,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl950_566])],[avatar_definition]) ).
fof(f88701,plain,
( ! [X0] :
( ~ r1_tarski(sK75,k3_subset_1(sK73,X0))
| r1_tarski(X0,sF947)
| ~ m1_subset_1(X0,sF948) )
| ~ spl950_566 ),
inference(avatar_component_clause,[],[f88700]) ).
fof(f88702,plain,
( ~ spl950_537
| spl950_566
| ~ spl950_525
| ~ spl950_534 ),
inference(avatar_split_clause,[],[f88692,f88357,f88241,f88700,f88405]) ).
fof(f89107,definition,
( spl950_591
<=> r1_xboole_0(sF945,sF944) ),
introduced(definition,[new_symbols(definition,[spl950_591])],[avatar_definition]) ).
fof(f89264,definition,
( spl950_612
<=> r1_xboole_0(sK75,sF946) ),
introduced(definition,[new_symbols(definition,[spl950_612])],[avatar_definition]) ).
fof(f89892,plain,
( ! [X0] :
( r1_xboole_0(sK75,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK73))
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ r1_tarski(X0,sF947)
| ~ m1_subset_1(X0,sF948) )
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(resolution,[],[f78076,f88316]) ).
fof(f89895,plain,
( ! [X0] :
( r1_xboole_0(sF945,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK72))
| ~ m1_subset_1(sF945,k1_zfmisc_1(sK72))
| ~ m1_subset_1(X0,sF949)
| ~ r1_tarski(X0,sK74) )
| ~ spl950_543 ),
inference(resolution,[],[f78076,f88451]) ).
fof(f89919,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF949)
| r1_xboole_0(sF945,X0)
| ~ m1_subset_1(sF945,k1_zfmisc_1(sK72))
| ~ m1_subset_1(X0,sF949)
| ~ r1_tarski(X0,sK74) )
| ~ spl950_526
| ~ spl950_543 ),
inference(forward_demodulation,[],[f89895,f88248]) ).
fof(f89920,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF949)
| r1_xboole_0(sF945,X0)
| ~ m1_subset_1(sF945,k1_zfmisc_1(sK72))
| ~ r1_tarski(X0,sK74) )
| ~ spl950_526
| ~ spl950_543 ),
inference(duplicate_literal_removal,[],[f89919]) ).
fof(f89923,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF948)
| r1_xboole_0(sK75,X0)
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ r1_tarski(X0,sF947)
| ~ m1_subset_1(X0,sF948) )
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_demodulation,[],[f89892,f88243]) ).
fof(f89924,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF948)
| r1_xboole_0(sK75,X0)
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ r1_tarski(X0,sF947) )
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(duplicate_literal_removal,[],[f89923]) ).
fof(f89938,plain,
( ! [X0] :
( ~ m1_subset_1(sF945,sF949)
| ~ m1_subset_1(X0,sF949)
| r1_xboole_0(sF945,X0)
| ~ r1_tarski(X0,sK74) )
| ~ spl950_526
| ~ spl950_543 ),
inference(forward_demodulation,[],[f89920,f88248]) ).
fof(f89941,plain,
( ! [X0] :
( ~ m1_subset_1(sK75,sF948)
| ~ m1_subset_1(X0,sF948)
| r1_xboole_0(sK75,X0)
| ~ r1_tarski(X0,sF947) )
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_demodulation,[],[f89924,f88243]) ).
fof(f89951,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF949)
| r1_xboole_0(sF945,X0)
| ~ r1_tarski(X0,sK74) )
| ~ spl950_526
| ~ spl950_538
| ~ spl950_543 ),
inference(forward_subsumption_resolution,[],[f89938,f88431]) ).
fof(f89954,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF948)
| r1_xboole_0(sK75,X0)
| ~ r1_tarski(X0,sF947) )
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525 ),
inference(forward_subsumption_resolution,[],[f89941,f88193]) ).
fof(f90489,plain,
( ! [X0] :
( ~ r1_xboole_0(sK75,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK73))
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| r1_tarski(X0,sF947)
| ~ m1_subset_1(X0,sF948) )
| ~ spl950_566 ),
inference(resolution,[],[f78075,f88701]) ).
fof(f90490,plain,
( ! [X0] :
( ~ r1_xboole_0(sF945,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK72))
| ~ m1_subset_1(sF945,k1_zfmisc_1(sK72))
| ~ m1_subset_1(X0,sF949)
| r1_tarski(X0,sK74) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(resolution,[],[f78075,f88303]) ).
fof(f90516,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF949)
| ~ r1_xboole_0(sF945,X0)
| ~ m1_subset_1(sF945,k1_zfmisc_1(sK72))
| ~ m1_subset_1(X0,sF949)
| r1_tarski(X0,sK74) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_demodulation,[],[f90490,f88248]) ).
fof(f90517,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF949)
| ~ r1_xboole_0(sF945,X0)
| ~ m1_subset_1(sF945,k1_zfmisc_1(sK72))
| r1_tarski(X0,sK74) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(duplicate_literal_removal,[],[f90516]) ).
fof(f90518,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF948)
| ~ r1_xboole_0(sK75,X0)
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| r1_tarski(X0,sF947)
| ~ m1_subset_1(X0,sF948) )
| ~ spl950_525
| ~ spl950_566 ),
inference(forward_demodulation,[],[f90489,f88243]) ).
fof(f90519,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF948)
| ~ r1_xboole_0(sK75,X0)
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| r1_tarski(X0,sF947) )
| ~ spl950_525
| ~ spl950_566 ),
inference(duplicate_literal_removal,[],[f90518]) ).
fof(f90530,plain,
( ! [X0] :
( ~ m1_subset_1(sF945,sF949)
| ~ m1_subset_1(X0,sF949)
| ~ r1_xboole_0(sF945,X0)
| r1_tarski(X0,sK74) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526 ),
inference(forward_demodulation,[],[f90517,f88248]) ).
fof(f90531,plain,
( ! [X0] :
( ~ m1_subset_1(sK75,sF948)
| ~ m1_subset_1(X0,sF948)
| ~ r1_xboole_0(sK75,X0)
| r1_tarski(X0,sF947) )
| ~ spl950_525
| ~ spl950_566 ),
inference(forward_demodulation,[],[f90519,f88243]) ).
fof(f90541,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF949)
| ~ r1_xboole_0(sF945,X0)
| r1_tarski(X0,sK74) )
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526
| ~ spl950_538 ),
inference(forward_subsumption_resolution,[],[f90530,f88431]) ).
fof(f90542,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF948)
| ~ r1_xboole_0(sK75,X0)
| r1_tarski(X0,sF947) )
| ~ spl950_515
| ~ spl950_525
| ~ spl950_566 ),
inference(forward_subsumption_resolution,[],[f90531,f88193]) ).
fof(f90557,plain,
( ~ r1_xboole_0(sK75,sF946)
| r1_tarski(sF946,sF947)
| ~ spl950_515
| ~ spl950_525
| ~ spl950_528
| ~ spl950_566 ),
inference(resolution,[],[f90542,f88264]) ).
fof(f91381,plain,
! [X2,X3,X0,X1,X4] :
( r1_xboole_0(X2,k9_relat_1(k4_relat_1(X1),X0))
| ~ r1_xboole_0(X0,k9_relat_1(X1,X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(X4))
| ~ m2_relset_1(X1,X4,X3) ),
inference(resolution,[],[f79024,f79013]) ).
fof(f91387,plain,
( ! [X2,X3,X0,X1] :
( ~ r1_xboole_0(X1,k9_relat_1(sK76,X0))
| r1_xboole_0(X0,k9_relat_1(sF943,X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X3))
| ~ m2_relset_1(sK76,X3,X2) )
| ~ spl950_532 ),
inference(superposition,[],[f91381,f88331]) ).
fof(f91390,plain,
( ! [X2,X0,X1] :
( r1_xboole_0(sF945,k9_relat_1(sF943,X0))
| ~ r1_xboole_0(X0,sF946)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ m1_subset_1(sF945,k1_zfmisc_1(X2))
| ~ m2_relset_1(sK76,X2,X1) )
| ~ spl950_532
| ~ spl950_545 ),
inference(superposition,[],[f91387,f88474]) ).
fof(f91391,plain,
( ! [X0,X1] :
( r1_xboole_0(sF945,sF944)
| ~ r1_xboole_0(sK75,sF946)
| ~ m1_subset_1(sK75,k1_zfmisc_1(X0))
| ~ m1_subset_1(sF945,k1_zfmisc_1(X1))
| ~ m2_relset_1(sK76,X1,X0) )
| ~ spl950_532
| ~ spl950_545
| ~ spl950_546 ),
inference(superposition,[],[f91390,f88479]) ).
fof(f91415,definition,
( spl950_742
<=> ! [X0,X1] :
( ~ m1_subset_1(sK75,k1_zfmisc_1(X0))
| ~ m1_subset_1(sF945,k1_zfmisc_1(X1))
| ~ m2_relset_1(sK76,X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl950_742])],[avatar_definition]) ).
fof(f91416,plain,
( ! [X0,X1] :
( ~ m2_relset_1(sK76,X1,X0)
| ~ m1_subset_1(sF945,k1_zfmisc_1(X1))
| ~ m1_subset_1(sK75,k1_zfmisc_1(X0)) )
| ~ spl950_742 ),
inference(avatar_component_clause,[],[f91415]) ).
fof(f91417,plain,
( spl950_742
| ~ spl950_612
| spl950_591
| ~ spl950_532
| ~ spl950_545
| ~ spl950_546 ),
inference(avatar_split_clause,[],[f91391,f88477,f88472,f88329,f89107,f89264,f91415]) ).
fof(f91840,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1_xboole_0(X0,k9_relat_1(k4_relat_1(X1),X2))
| r1_xboole_0(X2,k9_relat_1(X1,X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| ~ m1_subset_1(X0,k1_zfmisc_1(X4))
| ~ m2_relset_1(X1,X4,X3) ),
inference(resolution,[],[f79023,f79013]) ).
fof(f91847,plain,
( ! [X2,X3,X0,X1] :
( ~ r1_xboole_0(X0,k9_relat_1(sF943,X1))
| r1_xboole_0(X1,k9_relat_1(sK76,X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X3))
| ~ m2_relset_1(sK76,X3,X2) )
| ~ spl950_532 ),
inference(superposition,[],[f91840,f88331]) ).
fof(f91851,plain,
( ! [X2,X0,X1] :
( r1_xboole_0(sK75,k9_relat_1(sK76,X0))
| ~ r1_xboole_0(X0,sF944)
| ~ m1_subset_1(sK75,k1_zfmisc_1(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m2_relset_1(sK76,X2,X1) )
| ~ spl950_532
| ~ spl950_546 ),
inference(superposition,[],[f91847,f88479]) ).
fof(f91856,plain,
( ! [X0,X1] :
( r1_xboole_0(sK75,sF946)
| ~ r1_xboole_0(sF945,sF944)
| ~ m1_subset_1(sK75,k1_zfmisc_1(X0))
| ~ m1_subset_1(sF945,k1_zfmisc_1(X1))
| ~ m2_relset_1(sK76,X1,X0) )
| ~ spl950_532
| ~ spl950_545
| ~ spl950_546 ),
inference(superposition,[],[f91851,f88474]) ).
fof(f91857,plain,
( spl950_742
| ~ spl950_591
| spl950_612
| ~ spl950_532
| ~ spl950_545
| ~ spl950_546 ),
inference(avatar_split_clause,[],[f91856,f88477,f88472,f88329,f89264,f89107,f91415]) ).
fof(f92232,plain,
( spl950_517
| ~ spl950_612
| ~ spl950_515
| ~ spl950_525
| ~ spl950_528
| ~ spl950_566 ),
inference(avatar_split_clause,[],[f90557,f88700,f88262,f88241,f88191,f89264,f88201]) ).
fof(f92598,plain,
( ~ m1_subset_1(sF945,k1_zfmisc_1(sK72))
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ spl950_516
| ~ spl950_742 ),
inference(resolution,[],[f91416,f88198]) ).
fof(f92599,plain,
( ~ m1_subset_1(sF945,sF949)
| ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ spl950_516
| ~ spl950_526
| ~ spl950_742 ),
inference(forward_demodulation,[],[f92598,f88248]) ).
fof(f92600,plain,
( ~ m1_subset_1(sK75,k1_zfmisc_1(sK73))
| ~ spl950_516
| ~ spl950_526
| ~ spl950_538
| ~ spl950_742 ),
inference(forward_subsumption_resolution,[],[f92599,f88431]) ).
fof(f92601,plain,
( ~ m1_subset_1(sK75,sF948)
| ~ spl950_516
| ~ spl950_525
| ~ spl950_526
| ~ spl950_538
| ~ spl950_742 ),
inference(forward_demodulation,[],[f92600,f88243]) ).
fof(f92602,plain,
( $false
| ~ spl950_515
| ~ spl950_516
| ~ spl950_525
| ~ spl950_526
| ~ spl950_538
| ~ spl950_742 ),
inference(forward_subsumption_resolution,[],[f92601,f88193]) ).
fof(f92603,plain,
( ~ spl950_515
| ~ spl950_516
| ~ spl950_525
| ~ spl950_526
| ~ spl950_538
| ~ spl950_742 ),
inference(avatar_contradiction_clause,[],[f92602]) ).
fof(f92972,plain,
( ~ r1_xboole_0(sF945,sF944)
| r1_tarski(sF944,sK74)
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526
| ~ spl950_530
| ~ spl950_538 ),
inference(resolution,[],[f90541,f88273]) ).
fof(f93948,plain,
( r1_xboole_0(sK75,sF946)
| ~ r1_tarski(sF946,sF947)
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525
| ~ spl950_528 ),
inference(resolution,[],[f89954,f88264]) ).
fof(f94039,plain,
( spl950_518
| ~ spl950_591
| ~ spl950_514
| ~ spl950_522
| ~ spl950_526
| ~ spl950_530
| ~ spl950_538 ),
inference(avatar_split_clause,[],[f92972,f88430,f88271,f88246,f88226,f88186,f89107,f88205]) ).
fof(f94041,plain,
( ~ spl950_517
| spl950_612
| ~ spl950_515
| ~ spl950_524
| ~ spl950_525
| ~ spl950_528 ),
inference(avatar_split_clause,[],[f93948,f88262,f88241,f88236,f88191,f89264,f88201]) ).
fof(f101281,plain,
( r1_xboole_0(sF945,sF944)
| ~ r1_tarski(sF944,sK74)
| ~ spl950_526
| ~ spl950_530
| ~ spl950_538
| ~ spl950_543 ),
inference(resolution,[],[f89951,f88273]) ).
fof(f101283,plain,
( r1_xboole_0(sF945,sF944)
| ~ spl950_518
| ~ spl950_526
| ~ spl950_530
| ~ spl950_538
| ~ spl950_543 ),
inference(forward_subsumption_resolution,[],[f101281,f88207]) ).
fof(f101287,plain,
( spl950_591
| ~ spl950_518
| ~ spl950_526
| ~ spl950_530
| ~ spl950_538
| ~ spl950_543 ),
inference(avatar_split_clause,[],[f101283,f88450,f88430,f88271,f88246,f88205,f89107]) ).
cnf(s524,plain,
spl950_514,
inference(sat_conversion,[],[f88189]) ).
cnf(s525,plain,
spl950_515,
inference(sat_conversion,[],[f88194]) ).
cnf(s526,plain,
spl950_516,
inference(sat_conversion,[],[f88199]) ).
cnf(s527,plain,
( spl950_517
| spl950_518 ),
inference(sat_conversion,[],[f88208]) ).
cnf(s528,plain,
( ~ spl950_517
| ~ spl950_518 ),
inference(sat_conversion,[],[f88209]) ).
cnf(s530,plain,
spl950_520,
inference(sat_conversion,[],[f88219]) ).
cnf(s531,plain,
spl950_521,
inference(sat_conversion,[],[f88224]) ).
cnf(s532,plain,
spl950_522,
inference(sat_conversion,[],[f88229]) ).
cnf(s533,plain,
spl950_523,
inference(sat_conversion,[],[f88234]) ).
cnf(s534,plain,
spl950_524,
inference(sat_conversion,[],[f88239]) ).
cnf(s535,plain,
spl950_525,
inference(sat_conversion,[],[f88244]) ).
cnf(s536,plain,
spl950_526,
inference(sat_conversion,[],[f88249]) ).
cnf(s538,plain,
( ~ spl950_523
| ~ spl950_525
| ~ spl950_527
| spl950_528 ),
inference(sat_conversion,[],[f88265]) ).
cnf(s539,plain,
( ~ spl950_521
| ~ spl950_526
| ~ spl950_529
| spl950_530 ),
inference(sat_conversion,[],[f88274]) ).
cnf(s542,plain,
( ~ spl950_520
| ~ spl950_527
| spl950_532 ),
inference(sat_conversion,[],[f88333]) ).
cnf(s544,plain,
( ~ spl950_515
| ~ spl950_524
| ~ spl950_525
| spl950_534 ),
inference(sat_conversion,[],[f88360]) ).
cnf(s545,plain,
( ~ spl950_520
| ~ spl950_527
| spl950_535 ),
inference(sat_conversion,[],[f88368]) ).
cnf(s556,plain,
( ~ spl950_523
| ~ spl950_527
| spl950_545 ),
inference(sat_conversion,[],[f88481]) ).
cnf(s557,plain,
( ~ spl950_521
| ~ spl950_529
| spl950_546 ),
inference(sat_conversion,[],[f88482]) ).
cnf(s558,plain,
( ~ spl950_514
| ~ spl950_522
| ~ spl950_526
| spl950_543 ),
inference(sat_conversion,[],[f88483]) ).
cnf(s559,plain,
( ~ spl950_514
| ~ spl950_522
| ~ spl950_526
| spl950_538 ),
inference(sat_conversion,[],[f88497]) ).
cnf(s560,plain,
( ~ spl950_515
| ~ spl950_524
| ~ spl950_525
| spl950_537 ),
inference(sat_conversion,[],[f88498]) ).
cnf(s567,plain,
( ~ spl950_516
| spl950_527 ),
inference(sat_conversion,[],[f88578]) ).
cnf(s570,plain,
( spl950_529
| ~ spl950_535 ),
inference(sat_conversion,[],[f88594]) ).
cnf(s579,plain,
( ~ spl950_525
| ~ spl950_534
| ~ spl950_537
| spl950_566 ),
inference(sat_conversion,[],[f88702]) ).
cnf(s766,plain,
( ~ spl950_532
| ~ spl950_545
| ~ spl950_546
| spl950_591
| ~ spl950_612
| spl950_742 ),
inference(sat_conversion,[],[f91417]) ).
cnf(s808,plain,
( ~ spl950_532
| ~ spl950_545
| ~ spl950_546
| ~ spl950_591
| spl950_612
| spl950_742 ),
inference(sat_conversion,[],[f91857]) ).
cnf(s838,plain,
( ~ spl950_515
| spl950_517
| ~ spl950_525
| ~ spl950_528
| ~ spl950_566
| ~ spl950_612 ),
inference(sat_conversion,[],[f92232]) ).
cnf(s914,plain,
( ~ spl950_515
| ~ spl950_516
| ~ spl950_525
| ~ spl950_526
| ~ spl950_538
| ~ spl950_742 ),
inference(sat_conversion,[],[f92603]) ).
cnf(s1070,plain,
( ~ spl950_514
| spl950_518
| ~ spl950_522
| ~ spl950_526
| ~ spl950_530
| ~ spl950_538
| ~ spl950_591 ),
inference(sat_conversion,[],[f94039]) ).
cnf(s1071,plain,
( ~ spl950_515
| ~ spl950_517
| ~ spl950_524
| ~ spl950_525
| ~ spl950_528
| spl950_612 ),
inference(sat_conversion,[],[f94041]) ).
cnf(s1829,plain,
( ~ spl950_518
| ~ spl950_526
| ~ spl950_530
| ~ spl950_538
| ~ spl950_543
| spl950_591 ),
inference(sat_conversion,[],[f101287]) ).
cnf(s1838,plain,
spl950_527,
inference(rat,[],[s567,s526]) ).
cnf(s1843,plain,
spl950_545,
inference(rat,[],[s556,s533,s1838]) ).
cnf(s1844,plain,
spl950_535,
inference(rat,[],[s545,s530,s1838]) ).
cnf(s1845,plain,
spl950_532,
inference(rat,[],[s542,s530,s1838]) ).
cnf(s1846,plain,
spl950_528,
inference(rat,[],[s538,s533,s535,s1838]) ).
cnf(s1854,plain,
spl950_529,
inference(rat,[],[s570,s1844]) ).
cnf(s1863,plain,
spl950_546,
inference(rat,[],[s557,s531,s1854]) ).
cnf(s1864,plain,
spl950_530,
inference(rat,[],[s539,s531,s536,s1854]) ).
cnf(s1895,plain,
spl950_537,
inference(rat,[],[s560,s534,s535,s525]) ).
cnf(s1897,plain,
spl950_534,
inference(rat,[],[s544,s534,s535,s525]) ).
cnf(s1910,plain,
spl950_566,
inference(rat,[],[s579,s1895,s535,s1897]) ).
cnf(s1937,plain,
spl950_538,
inference(rat,[],[s559,s532,s536,s524]) ).
cnf(s1938,plain,
spl950_543,
inference(rat,[],[s558,s532,s536,s524]) ).
cnf(s1947,plain,
~ spl950_742,
inference(rat,[],[s914,s525,s526,s536,s535,s1937]) ).
cnf(s1985,plain,
spl950_517,
inference(rat,[],[s1829,s808,s527,s838,s536,s1864,s1938,s1937,s1843,s1845,s1863,s1947,s535,s1846,s525,s1910]) ).
cnf(s1986,plain,
spl950_612,
inference(rat,[],[s1071,s525,s1846,s535,s534,s1985]) ).
cnf(s1988,plain,
~ spl950_518,
inference(rat,[],[s528,s1985]) ).
cnf(s1991,plain,
spl950_591,
inference(rat,[],[s766,s1947,s1863,s1845,s1843,s1986]) ).
cnf(s1993,plain,
$false,
inference(rat,[],[s1070,s1937,s524,s1864,s536,s532,s1991,s1988]) ).
fof(f101294,plain,
$false,
inference(avatar_sat_refutation,[],[s1993]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU448+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n015.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 05:40:08 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 22.20/8.88 % (2321733)Detected formulas, will run a generic FOF schedule.
% 22.20/8.88 % (2321740)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=1295041203:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 22.20/8.88 % (2321738)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=2054185215:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 22.20/8.88 % (2321739)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=536752416:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 22.20/8.88 % (2321741)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1980228566:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 22.20/8.88 % (2321742)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1389477316:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 22.20/8.88 % (2321743)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2266302945:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 22.20/8.88 % (2321744)dis-21_1_sil=8000:lcm=predicate:random_seed=1800130876:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2944 on theBenchmark for (2944ds/129Mi)
% 22.20/8.88 % (2321741)Instruction limit reached!
% 22.20/8.88 % (2321741)------------------------------
% 22.20/8.88 % (2321741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/8.88 % (2321741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/8.88 % (2321741)CaDiCaL version: 2.1.3
% 22.20/8.88 % (2321741)Termination reason: Instruction limit
% 22.20/8.88 % (2321741)Termination phase: SInE selection
% 22.20/8.88 % (2321741)Time elapsed: 0.081 s
% 22.20/8.88 % (2321741)Peak memory usage: 201 MB
% 22.20/8.88 % (2321741)Instructions burned: 109 (million)
% 22.20/8.88 % (2321743)Instruction limit reached!
% 22.20/8.88 % (2321743)------------------------------
% 22.20/8.88 % (2321743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/8.88 % (2321743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/8.88 % (2321743)CaDiCaL version: 2.1.3
% 22.20/8.88 % (2321743)Termination reason: Instruction limit
% 22.20/8.88 % (2321743)Termination phase: Property scanning
% 22.20/8.88 % (2321743)Time elapsed: 0.067 s
% 22.20/8.88 % (2321743)Peak memory usage: 201 MB
% 22.20/8.88 % (2321743)Instructions burned: 139 (million)
% 22.20/8.88 % (2321742)Instruction limit reached!
% 22.20/8.88 % (2321742)------------------------------
% 22.20/8.88 % (2321742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/8.88 % (2321742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/8.88 % (2321742)CaDiCaL version: 2.1.3
% 22.20/8.88 % (2321742)Termination reason: Instruction limit
% 22.20/8.88 % (2321742)Termination phase: SInE selection
% 22.20/8.88 % (2321742)Time elapsed: 0.096 s
% 22.20/8.88 % (2321742)Peak memory usage: 201 MB
% 22.20/8.88 % (2321742)Instructions burned: 119 (million)
% 22.20/8.88 % (2321744)Instruction limit reached!
% 22.20/8.88 % (2321744)------------------------------
% 22.20/8.88 % (2321744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/8.88 % (2321744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/8.88 % (2321744)CaDiCaL version: 2.1.3
% 22.20/8.88 % (2321744)Termination reason: Instruction limit
% 22.20/8.88 % (2321744)Termination phase: SInE selection
% 22.20/8.88 % (2321744)Time elapsed: 0.103 s
% 22.20/8.88 % (2321744)Peak memory usage: 201 MB
% 22.20/8.88 % (2321744)Instructions burned: 129 (million)
% 22.20/8.88 % (2321752)lrs+10_1_sil=8000:sp=occurrence:random_seed=3379093278:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 22.20/8.88 % (2321753)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4290020382:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/157Mi)
% 22.20/8.88 % (2321754)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2513218091:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 22.20/8.88 % (2321755)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=2376718135:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 22.20/8.88 % (2321753)Instruction limit reached!
% 29.99/9.98 % (2321753)------------------------------
% 29.99/9.98 % (2321753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.99/9.98 % (2321753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.99/9.98 % (2321753)CaDiCaL version: 2.1.3
% 29.99/9.98 % (2321753)Termination reason: Instruction limit
% 29.99/9.98 % (2321753)Termination phase: Property scanning
% 29.99/9.98 % (2321753)Time elapsed: 0.076 s
% 29.99/9.98 % (2321753)Peak memory usage: 201 MB
% 29.99/9.98 % (2321753)Instructions burned: 159 (million)
% 29.99/9.98 % (2321755)Instruction limit reached!
% 29.99/9.98 % (2321755)------------------------------
% 29.99/9.98 % (2321755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.99/9.98 % (2321755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.99/9.98 % (2321755)CaDiCaL version: 2.1.3
% 29.99/9.98 % (2321755)Termination reason: Instruction limit
% 29.99/9.98 % (2321755)Termination phase: Property scanning
% 29.99/9.98 % (2321755)Time elapsed: 0.112 s
% 29.99/9.98 % (2321755)Peak memory usage: 201 MB
% 29.99/9.98 % (2321755)Instructions burned: 250 (million)
% 29.99/9.98 % (2321752)Instruction limit reached!
% 29.99/9.98 % (2321752)------------------------------
% 29.99/9.98 % (2321752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.99/9.98 % (2321752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.99/9.98 % (2321752)CaDiCaL version: 2.1.3
% 29.99/9.98 % (2321752)Termination reason: Instruction limit
% 29.99/9.98 % (2321752)Termination phase: SInE selection
% 29.99/9.98 % (2321752)Time elapsed: 0.218 s
% 29.99/9.98 % (2321752)Peak memory usage: 201 MB
% 29.99/9.98 % (2321752)Instructions burned: 286 (million)
% 29.99/9.98 % (2321754)Instruction limit reached!
% 29.99/9.98 % (2321754)------------------------------
% 29.99/9.98 % (2321754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.99/9.98 % (2321754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.99/9.98 % (2321754)CaDiCaL version: 2.1.3
% 29.99/9.98 % (2321754)Termination reason: Instruction limit
% 29.99/9.98 % (2321754)Termination phase: SInE selection
% 29.99/9.98 % (2321754)Time elapsed: 0.244 s
% 29.99/9.98 % (2321754)Peak memory usage: 201 MB
% 29.99/9.98 % (2321754)Instructions burned: 325 (million)
% 29.99/9.98 % (2321760)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=510698770:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2939 on theBenchmark for (2939ds/294Mi)
% 29.99/9.98 % (2321761)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=785466713:i=2350_2938 on theBenchmark for (2938ds/2350Mi)
% 29.99/9.98 % (2321762)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4180084321:cts=off:i=113:fsr=off:ss=included:sgt=4_2938 on theBenchmark for (2938ds/113Mi)
% 29.99/9.98 % (2321764)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=546362321:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 29.99/9.98 % (2321760)Instruction limit reached!
% 29.99/9.98 % (2321760)------------------------------
% 29.99/9.98 % (2321760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.99/9.98 % (2321760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.99/9.98 % (2321760)CaDiCaL version: 2.1.3
% 29.99/9.98 % (2321760)Termination reason: Instruction limit
% 29.99/9.98 % (2321760)Termination phase: SInE selection
% 29.99/9.98 % (2321760)Time elapsed: 0.231 s
% 29.99/9.98 % (2321760)Peak memory usage: 201 MB
% 29.99/9.98 % (2321760)Instructions burned: 295 (million)
% 29.99/9.98 % (2321762)Instruction limit reached!
% 29.99/9.98 % (2321762)------------------------------
% 29.99/9.98 % (2321762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.99/9.98 % (2321762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.99/9.98 % (2321762)CaDiCaL version: 2.1.3
% 29.99/9.98 % (2321762)Termination reason: Instruction limit
% 29.99/9.98 % (2321762)Termination phase: SInE selection
% 29.99/9.98 % (2321762)Time elapsed: 0.087 s
% 29.99/9.98 % (2321762)Peak memory usage: 201 MB
% 29.99/9.98 % (2321762)Instructions burned: 114 (million)
% 29.99/9.98 % (2321764)Instruction limit reached!
% 29.99/9.98 % (2321764)------------------------------
% 29.99/9.98 % (2321764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.99/9.98 % (2321764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.99/9.98 % (2321764)CaDiCaL version: 2.1.3
% 77.55/16.55 % (2321764)Termination reason: Instruction limit
% 77.55/16.55 % (2321764)Termination phase: Preprocessing 1
% 77.55/16.55 % (2321764)Time elapsed: 0.104 s
% 77.55/16.55 % (2321764)Peak memory usage: 202 MB
% 77.55/16.55 % (2321764)Instructions burned: 128 (million)
% 77.55/16.55 % (2321768)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1063944534:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2935 on theBenchmark for (2935ds/114Mi)
% 77.55/16.55 % (2321769)lrs+10_1_sil=8000:sp=occurrence:random_seed=2631144096:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2935 on theBenchmark for (2935ds/907Mi)
% 77.55/16.55 % (2321768)Instruction limit reached!
% 77.55/16.55 % (2321768)------------------------------
% 77.55/16.55 % (2321768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.55/16.55 % (2321768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.55/16.55 % (2321768)CaDiCaL version: 2.1.3
% 77.55/16.55 % (2321768)Termination reason: Instruction limit
% 77.55/16.55 % (2321768)Termination phase: Property scanning
% 77.55/16.55 % (2321768)Time elapsed: 0.057 s
% 77.55/16.55 % (2321768)Peak memory usage: 201 MB
% 77.55/16.55 % (2321768)Instructions burned: 116 (million)
% 77.55/16.55 % (2321770)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=198680543:i=437:sd=1:aac=none:ss=included_2934 on theBenchmark for (2934ds/437Mi)
% 77.55/16.55 % (2321773)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3876853044:i=5202:ss=axioms:sgt=16_2933 on theBenchmark for (2933ds/5202Mi)
% 77.55/16.55 % (2321770)Instruction limit reached!
% 77.55/16.55 % (2321770)------------------------------
% 77.55/16.55 % (2321770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.55/16.55 % (2321770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.55/16.55 % (2321770)CaDiCaL version: 2.1.3
% 77.55/16.55 % (2321770)Termination reason: Instruction limit
% 77.55/16.55 % (2321770)Termination phase: SInE selection
% 77.55/16.55 % (2321770)Time elapsed: 0.332 s
% 77.55/16.55 % (2321770)Peak memory usage: 202 MB
% 77.55/16.55 % (2321770)Instructions burned: 438 (million)
% 77.55/16.55 % (2321776)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2767666287:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2929 on theBenchmark for (2929ds/134Mi)
% 77.55/16.55 % (2321769)Instruction limit reached!
% 77.55/16.55 % (2321769)------------------------------
% 77.55/16.55 % (2321769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.55/16.55 % (2321769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.55/16.55 % (2321769)CaDiCaL version: 2.1.3
% 77.55/16.55 % (2321769)Termination reason: Instruction limit
% 77.55/16.55 % (2321769)Termination phase: Preprocessing 1
% 77.55/16.55 % (2321769)Time elapsed: 0.649 s
% 77.55/16.55 % (2321769)Peak memory usage: 204 MB
% 77.55/16.55 % (2321769)Instructions burned: 907 (million)
% 77.55/16.55 % (2321776)Instruction limit reached!
% 77.55/16.55 % (2321776)------------------------------
% 77.55/16.55 % (2321776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.55/16.55 % (2321776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.55/16.55 % (2321776)CaDiCaL version: 2.1.3
% 77.55/16.55 % (2321776)Termination reason: Instruction limit
% 77.55/16.55 % (2321776)Termination phase: SInE selection
% 77.55/16.55 % (2321776)Time elapsed: 0.107 s
% 77.55/16.55 % (2321776)Peak memory usage: 201 MB
% 77.55/16.55 % (2321776)Instructions burned: 135 (million)
% 77.55/16.55 % (2321778)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2711663208:st=8:i=592:sd=3:ep=RST:ss=axioms_2927 on theBenchmark for (2927ds/592Mi)
% 77.55/16.55 % (2321779)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=455623524:st=3:i=13193:sd=3:ss=axioms_2926 on theBenchmark for (2926ds/13193Mi)
% 77.55/16.55 % (2321778)Instruction limit reached!
% 77.55/16.55 % (2321778)------------------------------
% 77.55/16.55 % (2321778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.55/16.55 % (2321778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.55/16.55 % (2321778)CaDiCaL version: 2.1.3
% 77.55/16.55 % (2321778)Termination reason: Instruction limit
% 77.55/16.55 % (2321778)Termination phase: SInE selection
% 77.55/16.55 % (2321778)Time elapsed: 0.379 s
% 77.55/16.55 % (2321778)Peak memory usage: 203 MB
% 77.55/16.55 % (2321778)Instructions burned: 593 (million)
% 77.55/16.55 % (2321782)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=3060831582:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2921 on theBenchmark for (2921ds/125Mi)
% 100.97/19.87 % (2321782)Instruction limit reached!
% 100.97/19.87 % (2321782)------------------------------
% 100.97/19.87 % (2321782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.97/19.87 % (2321782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.97/19.87 % (2321782)CaDiCaL version: 2.1.3
% 100.97/19.87 % (2321782)Termination reason: Instruction limit
% 100.97/19.87 % (2321782)Termination phase: Property scanning
% 100.97/19.87 % (2321782)Time elapsed: 0.062 s
% 100.97/19.87 % (2321782)Peak memory usage: 201 MB
% 100.97/19.87 % (2321782)Instructions burned: 128 (million)
% 100.97/19.87 % (2321761)Instruction limit reached!
% 100.97/19.87 % (2321761)------------------------------
% 100.97/19.87 % (2321761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.97/19.87 % (2321761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.97/19.87 % (2321761)CaDiCaL version: 2.1.3
% 100.97/19.87 % (2321761)Termination reason: Instruction limit
% 100.97/19.87 % (2321761)Termination phase: Preprocessing 3
% 100.97/19.87 % (2321761)Time elapsed: 1.842 s
% 100.97/19.87 % (2321761)Peak memory usage: 305 MB
% 100.97/19.87 % (2321761)Instructions burned: 2350 (million)
% 100.97/19.87 % (2321784)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1337928078:i=134:gtgl=5:slsql=off:gtg=exists_sym_2919 on theBenchmark for (2919ds/134Mi)
% 100.97/19.87 % (2321784)Instruction limit reached!
% 100.97/19.87 % (2321784)------------------------------
% 100.97/19.87 % (2321784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.97/19.87 % (2321784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.97/19.87 % (2321784)CaDiCaL version: 2.1.3
% 100.97/19.87 % (2321784)Termination reason: Instruction limit
% 100.97/19.87 % (2321784)Termination phase: Property scanning
% 100.97/19.87 % (2321784)Time elapsed: 0.066 s
% 100.97/19.87 % (2321784)Peak memory usage: 201 MB
% 100.97/19.87 % (2321784)Instructions burned: 135 (million)
% 100.97/19.87 % (2321785)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2634469142:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2917 on theBenchmark for (2917ds/141Mi)
% 100.97/19.87 % (2321787)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1889882411:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2916 on theBenchmark for (2916ds/431Mi)
% 100.97/19.87 % (2321785)Instruction limit reached!
% 100.97/19.87 % (2321785)------------------------------
% 100.97/19.87 % (2321785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.97/19.87 % (2321785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.97/19.87 % (2321785)CaDiCaL version: 2.1.3
% 100.97/19.87 % (2321785)Termination reason: Instruction limit
% 100.97/19.87 % (2321785)Termination phase: SInE selection
% 100.97/19.87 % (2321785)Time elapsed: 0.108 s
% 100.97/19.87 % (2321785)Peak memory usage: 201 MB
% 100.97/19.87 % (2321785)Instructions burned: 141 (million)
% 100.97/19.87 % (2321790)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=1082347891:i=6060:aac=none:ins=25_2914 on theBenchmark for (2914ds/6060Mi)
% 100.97/19.87 % (2321787)Instruction limit reached!
% 100.97/19.87 % (2321787)------------------------------
% 100.97/19.87 % (2321787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.97/19.87 % (2321787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.97/19.87 % (2321787)CaDiCaL version: 2.1.3
% 100.97/19.87 % (2321787)Termination reason: Instruction limit
% 100.97/19.87 % (2321787)Termination phase: SInE selection
% 100.97/19.87 % (2321787)Time elapsed: 0.312 s
% 100.97/19.87 % (2321787)Peak memory usage: 202 MB
% 100.97/19.87 % (2321787)Instructions burned: 431 (million)
% 100.97/19.87 % (2321792)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=1331913841:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2911 on theBenchmark for (2911ds/150Mi)
% 100.97/19.87 % (2321792)Instruction limit reached!
% 100.97/19.87 % (2321792)------------------------------
% 100.97/19.87 % (2321792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.97/19.87 % (2321792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.97/19.87 % (2321792)CaDiCaL version: 2.1.3
% 100.97/19.87 % (2321792)Termination reason: Instruction limit
% 139.33/25.20 % (2321792)Termination phase: SInE selection
% 139.33/25.20 % (2321792)Time elapsed: 0.121 s
% 139.33/25.20 % (2321792)Peak memory usage: 201 MB
% 139.33/25.20 % (2321792)Instructions burned: 150 (million)
% 139.33/25.20 % (2321794)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3459124981:i=14155:bd=all_2908 on theBenchmark for (2908ds/14155Mi)
% 139.33/25.20 % (2321773)Instruction limit reached!
% 139.33/25.20 % (2321773)------------------------------
% 139.33/25.20 % (2321773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.33/25.20 % (2321773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.33/25.20 % (2321773)CaDiCaL version: 2.1.3
% 139.33/25.20 % (2321773)Termination reason: Instruction limit
% 139.33/25.20 % (2321773)Termination phase: Saturation
% 139.33/25.20 % (2321773)Time elapsed: 3.658 s
% 139.33/25.20 % (2321773)Peak memory usage: 424 MB
% 139.33/25.20 % (2321773)Instructions burned: 5203 (million)
% 139.33/25.20 % (2321796)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=79163012:i=667:av=off:fsr=off_2894 on theBenchmark for (2894ds/667Mi)
% 139.33/25.20 % (2321796)Instruction limit reached!
% 139.33/25.20 % (2321796)------------------------------
% 139.33/25.20 % (2321796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.33/25.20 % (2321796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.33/25.20 % (2321796)CaDiCaL version: 2.1.3
% 139.33/25.20 % (2321796)Termination reason: Instruction limit
% 139.33/25.20 % (2321796)Termination phase: Preprocessing 2
% 139.33/25.20 % (2321796)Time elapsed: 0.631 s
% 139.33/25.20 % (2321796)Peak memory usage: 218 MB
% 139.33/25.20 % (2321796)Instructions burned: 667 (million)
% 139.33/25.20 % (2321798)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=3322136623:s2a=on:i=185:s2at=1.8:fdi=4_2886 on theBenchmark for (2886ds/185Mi)
% 139.33/25.20 % (2321798)Instruction limit reached!
% 139.33/25.20 % (2321798)------------------------------
% 139.33/25.20 % (2321798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.33/25.20 % (2321798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.33/25.20 % (2321798)CaDiCaL version: 2.1.3
% 139.33/25.20 % (2321798)Termination reason: Instruction limit
% 139.33/25.20 % (2321798)Termination phase: SInE selection
% 139.33/25.20 % (2321798)Time elapsed: 0.145 s
% 139.33/25.20 % (2321798)Peak memory usage: 201 MB
% 139.33/25.20 % (2321798)Instructions burned: 185 (million)
% 139.33/25.20 % (2321800)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2935424934:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2882 on theBenchmark for (2882ds/193Mi)
% 139.33/25.20 % (2321800)Instruction limit reached!
% 139.33/25.20 % (2321800)------------------------------
% 139.33/25.20 % (2321800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.33/25.20 % (2321800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.33/25.20 % (2321800)CaDiCaL version: 2.1.3
% 139.33/25.20 % (2321800)Termination reason: Instruction limit
% 139.33/25.20 % (2321800)Termination phase: SInE selection
% 139.33/25.20 % (2321800)Time elapsed: 0.154 s
% 139.33/25.20 % (2321800)Peak memory usage: 201 MB
% 139.33/25.20 % (2321800)Instructions burned: 193 (million)
% 139.33/25.20 % (2321802)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=812792935:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2879 on theBenchmark for (2879ds/4850Mi)
% 139.33/25.20 % (2321790)Instruction limit reached!
% 139.33/25.20 % (2321790)------------------------------
% 139.33/25.20 % (2321790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.33/25.20 % (2321790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.33/25.20 % (2321790)CaDiCaL version: 2.1.3
% 139.33/25.20 % (2321790)Termination reason: Instruction limit
% 139.33/25.20 % (2321790)Termination phase: NewCNF
% 139.33/25.20 % (2321790)Time elapsed: 4.865 s
% 139.33/25.20 % (2321790)Peak memory usage: 381 MB
% 139.33/25.20 % (2321790)Instructions burned: 6060 (million)
% 139.33/25.20 % (2321804)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2100783408:i=12111:sd=1:ss=included_2863 on theBenchmark for (2863ds/12111Mi)
% 139.33/25.20 % (2321802)Instruction limit reached!
% 139.33/25.20 % (2321802)------------------------------
% 139.33/25.20 % (2321802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.69/30.12 % (2321802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.69/30.12 % (2321802)CaDiCaL version: 2.1.3
% 173.69/30.12 % (2321802)Termination reason: Instruction limit
% 173.69/30.12 % (2321802)Termination phase: Property scanning
% 173.69/30.12 % (2321802)Time elapsed: 3.458 s
% 173.69/30.12 % (2321802)Peak memory usage: 362 MB
% 173.69/30.12 % (2321802)Instructions burned: 4850 (million)
% 173.69/30.12 % (2321806)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1051683854:i=319:kws=precedence:fsr=off_2842 on theBenchmark for (2842ds/319Mi)
% 173.69/30.12 % (2321779)Instruction limit reached!
% 173.69/30.12 % (2321779)------------------------------
% 173.69/30.12 % (2321779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.69/30.12 % (2321779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.69/30.12 % (2321779)CaDiCaL version: 2.1.3
% 173.69/30.12 % (2321779)Termination reason: Instruction limit
% 173.69/30.12 % (2321779)Termination phase: Saturation
% 173.69/30.12 % (2321779)Time elapsed: 8.531 s
% 173.69/30.12 % (2321779)Peak memory usage: 674 MB
% 173.69/30.12 % (2321779)Instructions burned: 13195 (million)
% 173.69/30.12 % (2321806)Instruction limit reached!
% 173.69/30.12 % (2321806)------------------------------
% 173.69/30.12 % (2321806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.69/30.12 % (2321806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.69/30.12 % (2321806)CaDiCaL version: 2.1.3
% 173.69/30.12 % (2321806)Termination reason: Instruction limit
% 173.69/30.12 % (2321806)Termination phase: Preprocessing 1
% 173.69/30.12 % (2321806)Time elapsed: 0.239 s
% 173.69/30.12 % (2321806)Peak memory usage: 203 MB
% 173.69/30.12 % (2321806)Instructions burned: 320 (million)
% 173.69/30.12 % (2321808)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=926490088:i=2064:ep=RST_2839 on theBenchmark for (2839ds/2064Mi)
% 173.69/30.12 % (2321809)dis-1011_128_sil=32000:random_seed=1773712738:i=3706:ep=RST:av=off_2838 on theBenchmark for (2838ds/3706Mi)
% 173.69/30.12 % (2321794)Instruction limit reached!
% 173.69/30.12 % (2321794)------------------------------
% 173.69/30.12 % (2321794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.69/30.12 % (2321794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.69/30.12 % (2321794)CaDiCaL version: 2.1.3
% 173.69/30.12 % (2321794)Termination reason: Instruction limit
% 173.69/30.12 % (2321794)Termination phase: Property scanning
% 173.69/30.12 % (2321794)Time elapsed: 7.100 s
% 173.69/30.12 % (2321794)Peak memory usage: 447 MB
% 173.69/30.12 % (2321794)Instructions burned: 14155 (million)
% 173.69/30.12 % (2321812)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1310863296:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2835 on theBenchmark for (2835ds/757Mi)
% 173.69/30.12 % (2321812)Instruction limit reached!
% 173.69/30.12 % (2321812)------------------------------
% 173.69/30.12 % (2321812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.69/30.12 % (2321812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.69/30.12 % (2321812)CaDiCaL version: 2.1.3
% 173.69/30.12 % (2321812)Termination reason: Instruction limit
% 173.69/30.12 % (2321812)Termination phase: Saturation
% 173.69/30.12 % (2321812)Time elapsed: 0.605 s
% 173.69/30.12 % (2321812)Peak memory usage: 211 MB
% 173.69/30.12 % (2321812)Instructions burned: 757 (million)
% 173.69/30.12 % (2321814)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2416514603:i=13913:ss=axioms:sgt=8_2827 on theBenchmark for (2827ds/13913Mi)
% 173.69/30.12 % (2321808)Instruction limit reached!
% 173.69/30.12 % (2321808)------------------------------
% 173.69/30.12 % (2321808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.69/30.12 % (2321808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.69/30.12 % (2321808)CaDiCaL version: 2.1.3
% 173.69/30.12 % (2321808)Termination reason: Instruction limit
% 173.69/30.12 % (2321808)Termination phase: Preprocessing 3
% 173.69/30.12 % (2321808)Time elapsed: 1.694 s
% 173.69/30.12 % (2321808)Peak memory usage: 317 MB
% 173.69/30.12 % (2321808)Instructions burned: 2064 (million)
% 173.69/30.12 % (2321816)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3357486259:i=9925:aac=none_2820 on theBenchmark for (2820ds/9925Mi)
% 173.69/30.12 % (2321809)Instruction limit reached!
% 173.69/30.12 % (2321809)------------------------------
% 173.69/30.12 % (2321809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.18/35.12 % (2321809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.18/35.12 % (2321809)CaDiCaL version: 2.1.3
% 209.18/35.12 % (2321809)Termination reason: Instruction limit
% 209.18/35.12 % (2321809)Termination phase: Preprocessing 3
% 209.18/35.12 % (2321809)Time elapsed: 2.682 s
% 209.18/35.12 % (2321809)Peak memory usage: 378 MB
% 209.18/35.12 % (2321809)Instructions burned: 3706 (million)
% 209.18/35.12 % (2321818)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1516088983:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2809 on theBenchmark for (2809ds/2479Mi)
% 209.18/35.12 % (2321818)Instruction limit reached!
% 209.18/35.12 % (2321818)------------------------------
% 209.18/35.12 % (2321818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.18/35.12 % (2321818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.18/35.12 % (2321818)CaDiCaL version: 2.1.3
% 209.18/35.12 % (2321818)Termination reason: Instruction limit
% 209.18/35.12 % (2321818)Termination phase: Saturation
% 209.18/35.12 % (2321818)Time elapsed: 1.749 s
% 209.18/35.12 % (2321818)Peak memory usage: 223 MB
% 209.18/35.12 % (2321818)Instructions burned: 2480 (million)
% 209.18/35.12 % (2321820)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3450466265:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2790 on theBenchmark for (2790ds/440Mi)
% 209.18/35.12 % (2321820)Instruction limit reached!
% 209.18/35.12 % (2321820)------------------------------
% 209.18/35.12 % (2321820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.18/35.12 % (2321820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.18/35.12 % (2321820)CaDiCaL version: 2.1.3
% 209.18/35.12 % (2321820)Termination reason: Instruction limit
% 209.18/35.12 % (2321820)Termination phase: Property scanning
% 209.18/35.12 % (2321820)Time elapsed: 0.189 s
% 209.18/35.12 % (2321820)Peak memory usage: 201 MB
% 209.18/35.12 % (2321820)Instructions burned: 442 (million)
% 209.18/35.12 % (2321822)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3096609028:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2786 on theBenchmark for (2786ds/11145Mi)
% 209.18/35.12 % (2321804)Instruction limit reached!
% 209.18/35.12 % (2321804)------------------------------
% 209.18/35.12 % (2321804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.18/35.12 % (2321804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.18/35.12 % (2321804)CaDiCaL version: 2.1.3
% 209.18/35.12 % (2321804)Termination reason: Instruction limit
% 209.18/35.12 % (2321804)Termination phase: Saturation
% 209.18/35.12 % (2321804)Time elapsed: 8.099 s
% 209.18/35.12 % (2321804)Peak memory usage: 363 MB
% 209.18/35.12 % (2321804)Instructions burned: 12111 (million)
% 209.18/35.12 % (2321824)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=2214720403:cts=off:i=3034:av=off:er=known:fsd=on_2780 on theBenchmark for (2780ds/3034Mi)
% 209.18/35.12 % (2321816)Instruction limit reached!
% 209.18/35.12 % (2321816)------------------------------
% 209.18/35.12 % (2321816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.18/35.12 % (2321816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.18/35.12 % (2321816)CaDiCaL version: 2.1.3
% 209.18/35.12 % (2321816)Termination reason: Instruction limit
% 209.18/35.12 % (2321816)Termination phase: Property scanning
% 209.18/35.12 % (2321816)Time elapsed: 5.560 s
% 209.18/35.12 % (2321816)Peak memory usage: 447 MB
% 209.18/35.12 % (2321816)Instructions burned: 9928 (million)
% 209.18/35.12 % (2321826)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3104989478:st=2:s2a=on:i=524:s2at=2:ss=axioms_2762 on theBenchmark for (2762ds/524Mi)
% 209.18/35.12 % (2321826)Instruction limit reached!
% 209.18/35.12 % (2321826)------------------------------
% 209.18/35.12 % (2321826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.18/35.12 % (2321826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.18/35.12 % (2321826)CaDiCaL version: 2.1.3
% 209.18/35.12 % (2321826)Termination reason: Instruction limit
% 209.18/35.12 % (2321826)Termination phase: SInE selection
% 209.18/35.12 % (2321826)Time elapsed: 0.371 s
% 209.18/35.12 % (2321826)Peak memory usage: 202 MB
% 209.18/35.12 % (2321826)Instructions burned: 525 (million)
% 209.18/35.12 % (2321824)Instruction limit reached!
% 209.18/35.12 % (2321824)------------------------------
% 209.18/35.12 % (2321824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321824)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321824)Termination reason: Instruction limit
% 123.41/36.26 % (2321824)Termination phase: Preprocessing 3
% 123.41/36.26 % (2321824)Time elapsed: 2.243 s
% 123.41/36.26 % (2321824)Peak memory usage: 337 MB
% 123.41/36.26 % (2321824)Instructions burned: 3035 (million)
% 123.41/36.26 % (2321828)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1503609773:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2756 on theBenchmark for (2756ds/1016Mi)
% 123.41/36.26 % (2321829)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1318314646:i=14123:bd=preordered:ins=4_2756 on theBenchmark for (2756ds/14123Mi)
% 123.41/36.26 % (2321828)Instruction limit reached!
% 123.41/36.26 % (2321828)------------------------------
% 123.41/36.26 % (2321828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321828)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321828)Termination reason: Instruction limit
% 123.41/36.26 % (2321828)Termination phase: Saturation
% 123.41/36.26 % (2321828)Time elapsed: 0.773 s
% 123.41/36.26 % (2321828)Peak memory usage: 216 MB
% 123.41/36.26 % (2321828)Instructions burned: 1020 (million)
% 123.41/36.26 % (2321832)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3078232706:i=5781:kws=precedence:bd=all:rawr=on_2747 on theBenchmark for (2747ds/5781Mi)
% 123.41/36.26 % (2321814)Instruction limit reached!
% 123.41/36.26 % (2321814)------------------------------
% 123.41/36.26 % (2321814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321814)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321814)Termination reason: Instruction limit
% 123.41/36.26 % (2321814)Termination phase: Saturation
% 123.41/36.26 % (2321814)Time elapsed: 8.787 s
% 123.41/36.26 % (2321814)Peak memory usage: 448 MB
% 123.41/36.26 % (2321814)Instructions burned: 13913 (million)
% 123.41/36.26 % (2321834)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=1927183979:i=2448:gtgl=5:bd=preordered:gtg=all_2737 on theBenchmark for (2737ds/2448Mi)
% 123.41/36.26 % (2321834)Instruction limit reached!
% 123.41/36.26 % (2321834)------------------------------
% 123.41/36.26 % (2321834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321834)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321834)Termination reason: Instruction limit
% 123.41/36.26 % (2321834)Termination phase: Property scanning
% 123.41/36.26 % (2321834)Time elapsed: 1.031 s
% 123.41/36.26 % (2321834)Peak memory usage: 201 MB
% 123.41/36.26 % (2321834)Instructions burned: 2449 (million)
% 123.41/36.26 % (2321836)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3008819147:i=3223:kws=precedence:fgj=on:av=off_2725 on theBenchmark for (2725ds/3223Mi)
% 123.41/36.26 % (2321822)Instruction limit reached!
% 123.41/36.26 % (2321822)------------------------------
% 123.41/36.26 % (2321822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321822)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321822)Termination reason: Instruction limit
% 123.41/36.26 % (2321822)Termination phase: Saturation
% 123.41/36.26 % (2321822)Time elapsed: 7.381 s
% 123.41/36.26 % (2321822)Peak memory usage: 398 MB
% 123.41/36.26 % (2321822)Instructions burned: 11146 (million)
% 123.41/36.26 % (2321838)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4291627857:st=5.6:i=2033:sd=3:ss=axioms_2710 on theBenchmark for (2710ds/2033Mi)
% 123.41/36.26 % (2321832)Instruction limit reached!
% 123.41/36.26 % (2321832)------------------------------
% 123.41/36.26 % (2321832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321832)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321832)Termination reason: Instruction limit
% 123.41/36.26 % (2321832)Termination phase: Property scanning
% 123.41/36.26 % (2321832)Time elapsed: 3.788 s
% 123.41/36.26 % (2321832)Peak memory usage: 412 MB
% 123.41/36.26 % (2321832)Instructions burned: 5783 (million)
% 123.41/36.26 % (2321840)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3701728040:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2707 on theBenchmark for (2707ds/2055Mi)
% 123.41/36.26 % (2321836)Instruction limit reached!
% 123.41/36.26 % (2321836)------------------------------
% 123.41/36.26 % (2321836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321836)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321836)Termination reason: Instruction limit
% 123.41/36.26 % (2321836)Termination phase: Preprocessing 3
% 123.41/36.26 % (2321836)Time elapsed: 2.346 s
% 123.41/36.26 % (2321836)Peak memory usage: 342 MB
% 123.41/36.26 % (2321836)Instructions burned: 3224 (million)
% 123.41/36.26 % (2321842)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=3332619473:i=21611:sd=3:ss=axioms_2699 on theBenchmark for (2699ds/21611Mi)
% 123.41/36.26 % (2321840)Instruction limit reached!
% 123.41/36.26 % (2321840)------------------------------
% 123.41/36.26 % (2321840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321840)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321840)Termination reason: Instruction limit
% 123.41/36.26 % (2321840)Termination phase: SInE selection
% 123.41/36.26 % (2321840)Time elapsed: 1.019 s
% 123.41/36.26 % (2321840)Peak memory usage: 203 MB
% 123.41/36.26 % (2321840)Instructions burned: 2055 (million)
% 123.41/36.26 % (2321838)Instruction limit reached!
% 123.41/36.26 % (2321838)------------------------------
% 123.41/36.26 % (2321838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321838)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321838)Termination reason: Instruction limit
% 123.41/36.26 % (2321838)Termination phase: Naming
% 123.41/36.26 % (2321838)Time elapsed: 1.557 s
% 123.41/36.26 % (2321838)Peak memory usage: 237 MB
% 123.41/36.26 % (2321838)Instructions burned: 2033 (million)
% 123.41/36.26 % (2321844)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3946751335:i=4835:sd=13:ss=axioms:sgt=23_2694 on theBenchmark for (2694ds/4835Mi)
% 123.41/36.26 % (2321846)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=1223786739:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2693 on theBenchmark for (2693ds/797Mi)
% 123.41/36.26 % (2321846)Instruction limit reached!
% 123.41/36.26 % (2321846)------------------------------
% 123.41/36.26 % (2321846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321846)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321846)Termination reason: Instruction limit
% 123.41/36.26 % (2321846)Termination phase: SInE selection
% 123.41/36.26 % (2321846)Time elapsed: 0.518 s
% 123.41/36.26 % (2321846)Peak memory usage: 203 MB
% 123.41/36.26 % (2321846)Instructions burned: 798 (million)
% 123.41/36.26 % (2321848)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1721004714:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2686 on theBenchmark for (2686ds/2326Mi)
% 123.41/36.26 % (2321848)Instruction limit reached!
% 123.41/36.26 % (2321848)------------------------------
% 123.41/36.26 % (2321848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321848)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321848)Termination reason: Instruction limit
% 123.41/36.26 % (2321848)Termination phase: Preprocessing 3
% 123.41/36.26 % (2321848)Time elapsed: 1.881 s
% 123.41/36.26 % (2321848)Peak memory usage: 335 MB
% 123.41/36.26 % (2321848)Instructions burned: 2326 (million)
% 123.41/36.26 % (2321850)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2218036067:i=6038:nm=6_2665 on theBenchmark for (2665ds/6038Mi)
% 123.41/36.26 % (2321844)Instruction limit reached!
% 123.41/36.26 % (2321844)------------------------------
% 123.41/36.26 % (2321844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321844)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321844)Termination reason: Instruction limit
% 123.41/36.26 % (2321844)Termination phase: Property scanning
% 123.41/36.26 % (2321844)Time elapsed: 3.569 s
% 123.41/36.26 % (2321844)Peak memory usage: 372 MB
% 123.41/36.26 % (2321844)Instructions burned: 4835 (million)
% 123.41/36.26 % (2321852)lrs+10_1_sil=32000:sp=occurrence:random_seed=2103265142:st=2:i=33334:sd=3:ss=included:sgt=32_2657 on theBenchmark for (2657ds/33334Mi)
% 123.41/36.26 % (2321829)Instruction limit reached!
% 123.41/36.26 % (2321829)------------------------------
% 123.41/36.26 % (2321829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.41/36.26 % (2321829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.41/36.26 % (2321829)CaDiCaL version: 2.1.3
% 123.41/36.26 % (2321829)Termination reason: Instruction limit
% 123.41/36.26 % (2321829)Termination phase: Saturation
% 123.41/36.26 % (2321829)Time elapsed: 10.086 s
% 123.41/36.26 % (2321829)Peak memory usage: 1216 MB
% 123.41/36.26 % (2321829)Instructions burned: 14125 (million)
% 123.41/36.26 % (2321842)First to succeed.
% 123.41/36.26 % (2321842)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2321733"
% 123.41/36.26 % (2321854)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3827988633:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2652 on theBenchmark for (2652ds/1008Mi)
% 123.41/36.26 % (2321842)Refutation found. Thanks to Tanya!
% 123.41/36.26 % SZS status Theorem for theBenchmark
% 123.41/36.26 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/36.53 % (2321842)------------------------------
% 0.17/36.53 % (2321842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/36.53 % (2321842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/36.53 % (2321842)CaDiCaL version: 2.1.3
% 0.17/36.53 % (2321842)Termination reason: Refutation
% 0.17/36.53 % (2321842)Time elapsed: 4.683 s
% 0.17/36.53 % (2321842)Peak memory usage: 356 MB
% 0.17/36.53 % (2321842)Instructions burned: 7003 (million)
% 0.17/36.53 % (2321842)------------------------------
% 0.17/36.53 % (2321842)------------------------------
% 0.17/36.53 % (2321733)Success in time 35.396 s
% 0.17/36.53 % Vampire exiting
%------------------------------------------------------------------------------