%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU417+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 : n002.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:48:51 PM UTC 2026
% Result : Theorem 57.67s 16.57s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 18
% Syntax : Number of formulae : 111 ( 49 unt; 2 def)
% Number of atoms : 229 ( 56 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 215 ( 97 ~; 89 |; 10 &)
% ( 2 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-3 aty)
% Number of variables : 170 ( 0 sgn 167 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21,axiom,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f54,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(f98,axiom,
! [X0,X1,X2] : r1_tarski(k3_xboole_0(X0,X1),k2_xboole_0(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_xboole_1) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f567,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_subset_1) ).
fof(f570,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
fof(f571,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_subset_1) ).
fof(f574,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f601,axiom,
! [X0] : k1_setfam_1(k1_tarski(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_setfam_1) ).
fof(f602,axiom,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_setfam_1) ).
fof(f658,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ( r1_tarski(X1,X2)
=> r1_tarski(k8_setfam_1(X0,X2),k8_setfam_1(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_setfam_1) ).
fof(f16649,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ( X1 = k4_subset_1(k1_zfmisc_1(X0),X2,X3)
=> k8_setfam_1(X0,X1) = k5_subset_1(X0,k8_setfam_1(X0,X2),k8_setfam_1(X0,X3)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_mssubfam) ).
fof(f71063,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
& m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) )
=> m1_subset_1(k1_relset_2(X0,X1,X2),k1_zfmisc_1(k1_zfmisc_1(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_relset_2) ).
fof(f71066,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
& m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) )
=> k1_relset_2(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_relset_2) ).
fof(f71085,conjecture,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> r1_tarski(k5_subset_1(X0,k8_setfam_1(X0,X1),k8_setfam_1(X0,X2)),k8_setfam_1(X0,k1_relset_2(X0,X1,X2))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_relset_2) ).
fof(f71086,negated_conjecture,
~ ! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> r1_tarski(k5_subset_1(X0,k8_setfam_1(X0,X1),k8_setfam_1(X0,X2)),k8_setfam_1(X0,k1_relset_2(X0,X1,X2))) ) ),
inference(negated_conjecture,[status(cth)],[f71085]) ).
fof(f71284,plain,
! [X0,X1,X2] :
( m1_subset_1(k1_relset_2(X0,X1,X2),k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f71063]) ).
fof(f71285,plain,
! [X0,X1,X2] :
( m1_subset_1(k1_relset_2(X0,X1,X2),k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(flattening,[],[f71284]) ).
fof(f71290,plain,
! [X0,X1,X2] :
( k1_relset_2(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f71066]) ).
fof(f71291,plain,
! [X0,X1,X2] :
( k1_relset_2(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(flattening,[],[f71290]) ).
fof(f71309,plain,
? [X0,X1] :
( ? [X2] :
( ~ r1_tarski(k5_subset_1(X0,k8_setfam_1(X0,X1),k8_setfam_1(X0,X2)),k8_setfam_1(X0,k1_relset_2(X0,X1,X2)))
& m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) )
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f71086]) ).
fof(f71366,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f574]) ).
fof(f71367,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f71366]) ).
fof(f71852,plain,
! [X0,X1,X2] :
( m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f571]) ).
fof(f71853,plain,
! [X0,X1,X2] :
( m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f71852]) ).
fof(f71875,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( k8_setfam_1(X0,X1) = k5_subset_1(X0,k8_setfam_1(X0,X2),k8_setfam_1(X0,X3))
| k4_subset_1(k1_zfmisc_1(X0),X2,X3) != X1
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f16649]) ).
fof(f71876,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( k8_setfam_1(X0,X1) = k5_subset_1(X0,k8_setfam_1(X0,X2),k8_setfam_1(X0,X3))
| k4_subset_1(k1_zfmisc_1(X0),X2,X3) != X1
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(flattening,[],[f71875]) ).
fof(f71892,plain,
! [X0,X1] :
( ! [X2] :
( r1_tarski(k8_setfam_1(X0,X2),k8_setfam_1(X0,X1))
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f658]) ).
fof(f71893,plain,
! [X0,X1] :
( ! [X2] :
( r1_tarski(k8_setfam_1(X0,X2),k8_setfam_1(X0,X1))
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(flattening,[],[f71892]) ).
fof(f73886,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f570]) ).
fof(f73887,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f73886]) ).
fof(f73892,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f567]) ).
fof(f73893,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f73892]) ).
fof(f84142,plain,
( ~ r1_tarski(k5_subset_1(sK74,k8_setfam_1(sK74,sK75),k8_setfam_1(sK74,sK76)),k8_setfam_1(sK74,k1_relset_2(sK74,sK75,sK76)))
& m1_subset_1(sK76,k1_zfmisc_1(k1_zfmisc_1(sK74)))
& m1_subset_1(sK75,k1_zfmisc_1(k1_zfmisc_1(sK74))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK74,sK75,sK76]),skolemize(X0,sK74),skolemize(X1,sK75),skolemize(X2,sK76)],[f71309]) ).
fof(f87375,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| m1_subset_1(k1_relset_2(X0,X1,X2),k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f71285]) ).
fof(f87378,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k1_relset_2(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f71291]) ).
fof(f87403,plain,
m1_subset_1(sK75,k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(cnf_transformation,[],[f84142]) ).
fof(f87404,plain,
m1_subset_1(sK76,k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(cnf_transformation,[],[f84142]) ).
fof(f87405,plain,
~ r1_tarski(k5_subset_1(sK74,k8_setfam_1(sK74,sK75),k8_setfam_1(sK74,sK76)),k8_setfam_1(sK74,k1_relset_2(sK74,sK75,sK76))),
inference(cnf_transformation,[],[f84142]) ).
fof(f87468,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k5_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f71367]) ).
fof(f87501,plain,
! [X2,X0,X1] : r1_tarski(k3_xboole_0(X0,X1),k2_xboole_0(X0,X2)),
inference(cnf_transformation,[],[f98]) ).
fof(f88013,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
inference(cnf_transformation,[],[f54]) ).
fof(f88142,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f88213,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f71853]) ).
fof(f88263,plain,
! [X2,X3,X0,X1] :
( k8_setfam_1(X0,X1) = k5_subset_1(X0,k8_setfam_1(X0,X2),k8_setfam_1(X0,X3))
| k4_subset_1(k1_zfmisc_1(X0),X2,X3) != X1
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f71876]) ).
fof(f88274,plain,
! [X2,X0,X1] :
( r1_tarski(k8_setfam_1(X0,X2),k8_setfam_1(X0,X1))
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f71893]) ).
fof(f89202,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f89203,plain,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f21]) ).
fof(f91167,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k2_xboole_0(X1,X2) = k4_subset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f73887]) ).
fof(f91170,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f73893]) ).
fof(f94651,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k1_setfam_1(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f602]) ).
fof(f94652,plain,
! [X0] : k1_setfam_1(k1_tarski(X0)) = X0,
inference(cnf_transformation,[],[f601]) ).
fof(f105486,plain,
! [X2,X0,X1] :
( k1_relset_2(X0,X1,X2) = k4_xboole_0(X1,k4_xboole_0(X1,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(definition_unfolding,[],[f87378,f88142]) ).
fof(f105549,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k4_xboole_0(X1,k4_xboole_0(X1,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(definition_unfolding,[],[f87468,f88142]) ).
fof(f105582,plain,
! [X2,X0,X1] : r1_tarski(k4_xboole_0(X0,k4_xboole_0(X0,X1)),k2_xboole_0(X0,X2)),
inference(definition_unfolding,[],[f87501,f88142]) ).
fof(f107695,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k1_setfam_1(k2_tarski(X0,X1)),
inference(definition_unfolding,[],[f94651,f88142]) ).
fof(f107696,plain,
! [X0] : k1_setfam_1(k2_tarski(X0,X0)) = X0,
inference(definition_unfolding,[],[f94652,f89202]) ).
fof(f112761,plain,
! [X2,X3,X0] :
( k5_subset_1(X0,k8_setfam_1(X0,X2),k8_setfam_1(X0,X3)) = k8_setfam_1(X0,k4_subset_1(k1_zfmisc_1(X0),X2,X3))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(k4_subset_1(k1_zfmisc_1(X0),X2,X3),k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(equality_resolution,[],[f88263]) ).
fof(f115998,plain,
! [X2,X3,X0] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(X0)))
| k5_subset_1(X0,k8_setfam_1(X0,X2),k8_setfam_1(X0,X3)) = k8_setfam_1(X0,k4_subset_1(k1_zfmisc_1(X0),X2,X3)) ),
inference(forward_subsumption_resolution,[],[f112761,f91170]) ).
fof(f116105,plain,
! [X2,X0,X1] : r1_tarski(k1_setfam_1(k2_tarski(X0,X1)),k2_xboole_0(X0,X2)),
inference(forward_demodulation,[],[f105582,f107695]) ).
fof(f116136,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k5_subset_1(X0,X1,X2) = k1_setfam_1(k2_tarski(X1,X2)) ),
inference(forward_demodulation,[],[f105549,f107695]) ).
fof(f116185,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| k1_relset_2(X0,X1,X2) = k1_setfam_1(k2_tarski(X1,X2)) ),
inference(forward_demodulation,[],[f105486,f107695]) ).
fof(f118980,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(sK74)))
| k5_subset_1(k1_zfmisc_1(sK74),X0,sK75) = k1_setfam_1(k2_tarski(X0,sK75)) ),
inference(resolution,[],[f116136,f87403]) ).
fof(f118983,plain,
k5_subset_1(k1_zfmisc_1(sK74),sK76,sK75) = k1_setfam_1(k2_tarski(sK76,sK75)),
inference(resolution,[],[f118980,f87404]) ).
fof(f118984,plain,
k5_subset_1(k1_zfmisc_1(sK74),sK76,sK75) = k1_setfam_1(k2_tarski(sK75,sK76)),
inference(forward_demodulation,[],[f118983,f89203]) ).
fof(f118989,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(sK74)))
| m1_subset_1(k5_subset_1(k1_zfmisc_1(sK74),X0,sK75),k1_zfmisc_1(k1_zfmisc_1(sK74))) ),
inference(resolution,[],[f88213,f87403]) ).
fof(f118992,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(sK74)))
| m1_subset_1(k1_relset_2(sK74,X0,sK76),k1_zfmisc_1(k1_zfmisc_1(sK74))) ),
inference(resolution,[],[f87375,f87404]) ).
fof(f118994,plain,
m1_subset_1(k1_relset_2(sK74,sK76,sK76),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(resolution,[],[f118992,f87404]) ).
fof(f119003,plain,
m1_subset_1(k1_relset_2(sK74,k1_relset_2(sK74,sK76,sK76),sK76),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(resolution,[],[f118994,f118992]) ).
fof(f119044,plain,
m1_subset_1(k5_subset_1(k1_zfmisc_1(sK74),sK76,sK75),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(resolution,[],[f118989,f87404]) ).
fof(f119053,plain,
m1_subset_1(k1_setfam_1(k2_tarski(sK75,sK76)),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(forward_demodulation,[],[f119044,f118984]) ).
fof(f119088,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(sK74)))
| k1_setfam_1(k2_tarski(X0,sK76)) = k1_relset_2(sK74,X0,sK76) ),
inference(resolution,[],[f116185,f87404]) ).
fof(f119093,plain,
k1_relset_2(sK74,sK75,sK76) = k1_setfam_1(k2_tarski(sK75,sK76)),
inference(resolution,[],[f119088,f87403]) ).
fof(f119094,plain,
k1_setfam_1(k2_tarski(sK76,sK76)) = k1_relset_2(sK74,sK76,sK76),
inference(resolution,[],[f119088,f87404]) ).
fof(f119096,plain,
k1_relset_2(sK74,k1_relset_2(sK74,sK76,sK76),sK76) = k1_setfam_1(k2_tarski(k1_relset_2(sK74,sK76,sK76),sK76)),
inference(resolution,[],[f119088,f118994]) ).
fof(f119101,plain,
k1_relset_2(sK74,k1_relset_2(sK74,sK76,sK76),sK76) = k1_setfam_1(k2_tarski(sK76,k1_relset_2(sK74,sK76,sK76))),
inference(forward_demodulation,[],[f119096,f89203]) ).
fof(f119103,plain,
sK76 = k1_relset_2(sK74,sK76,sK76),
inference(forward_demodulation,[],[f119094,f107696]) ).
fof(f119121,plain,
~ r1_tarski(k5_subset_1(sK74,k8_setfam_1(sK74,sK75),k8_setfam_1(sK74,sK76)),k8_setfam_1(sK74,k1_setfam_1(k2_tarski(sK75,sK76)))),
inference(superposition,[],[f87405,f119093]) ).
fof(f120248,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(sK74)))
| k5_subset_1(sK74,k8_setfam_1(sK74,sK75),k8_setfam_1(sK74,X0)) = k8_setfam_1(sK74,k4_subset_1(k1_zfmisc_1(sK74),sK75,X0)) ),
inference(resolution,[],[f115998,f87403]) ).
fof(f120287,plain,
k5_subset_1(sK74,k8_setfam_1(sK74,sK75),k8_setfam_1(sK74,sK76)) = k8_setfam_1(sK74,k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76)),
inference(resolution,[],[f120248,f87404]) ).
fof(f120312,plain,
~ r1_tarski(k8_setfam_1(sK74,k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76)),k8_setfam_1(sK74,k1_setfam_1(k2_tarski(sK75,sK76)))),
inference(superposition,[],[f119121,f120287]) ).
fof(f120385,plain,
( ~ r1_tarski(k1_setfam_1(k2_tarski(sK75,sK76)),k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76))
| ~ m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76),k1_zfmisc_1(k1_zfmisc_1(sK74)))
| ~ m1_subset_1(k1_setfam_1(k2_tarski(sK75,sK76)),k1_zfmisc_1(k1_zfmisc_1(sK74))) ),
inference(resolution,[],[f120312,f88274]) ).
fof(f120388,definition,
( spl2393_138
<=> m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76),k1_zfmisc_1(k1_zfmisc_1(sK74))) ),
introduced(definition,[new_symbols(definition,[spl2393_138])],[avatar_definition]) ).
fof(f120389,plain,
( ~ m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76),k1_zfmisc_1(k1_zfmisc_1(sK74)))
| spl2393_138 ),
inference(avatar_component_clause,[],[f120388]) ).
fof(f120394,plain,
( ~ r1_tarski(k1_setfam_1(k2_tarski(sK75,sK76)),k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76))
| ~ m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76),k1_zfmisc_1(k1_zfmisc_1(sK74))) ),
inference(forward_subsumption_resolution,[],[f120385,f119053]) ).
fof(f120396,definition,
( spl2393_140
<=> r1_tarski(k1_setfam_1(k2_tarski(sK75,sK76)),k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76)) ),
introduced(definition,[new_symbols(definition,[spl2393_140])],[avatar_definition]) ).
fof(f120397,plain,
( ~ r1_tarski(k1_setfam_1(k2_tarski(sK75,sK76)),k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76))
| spl2393_140 ),
inference(avatar_component_clause,[],[f120396]) ).
fof(f120398,plain,
( ~ spl2393_138
| ~ spl2393_140 ),
inference(avatar_split_clause,[],[f120394,f120396,f120388]) ).
fof(f121936,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(sK74)))
| k2_xboole_0(X0,sK75) = k4_subset_1(k1_zfmisc_1(sK74),X0,sK75) ),
inference(resolution,[],[f91167,f87403]) ).
fof(f121937,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(sK74)))
| k2_xboole_0(X0,sK76) = k4_subset_1(k1_zfmisc_1(sK74),X0,sK76) ),
inference(resolution,[],[f91167,f87404]) ).
fof(f121995,plain,
k4_subset_1(k1_zfmisc_1(sK74),sK75,sK76) = k2_xboole_0(sK75,sK76),
inference(resolution,[],[f121937,f87403]) ).
fof(f122046,plain,
( ~ m1_subset_1(k2_xboole_0(sK75,sK76),k1_zfmisc_1(k1_zfmisc_1(sK74)))
| spl2393_138 ),
inference(superposition,[],[f120389,f121995]) ).
fof(f122063,plain,
k4_subset_1(k1_zfmisc_1(sK74),sK76,sK75) = k2_xboole_0(sK76,sK75),
inference(resolution,[],[f121936,f87404]) ).
fof(f122067,plain,
k4_subset_1(k1_zfmisc_1(sK74),sK76,sK75) = k2_xboole_0(sK75,sK76),
inference(forward_demodulation,[],[f122063,f88013]) ).
fof(f127216,plain,
( ~ r1_tarski(k1_setfam_1(k2_tarski(sK75,sK76)),k2_xboole_0(sK75,sK76))
| spl2393_140 ),
inference(forward_demodulation,[],[f120397,f121995]) ).
fof(f127275,plain,
( $false
| spl2393_140 ),
inference(forward_subsumption_resolution,[],[f127216,f116105]) ).
fof(f127276,plain,
spl2393_140,
inference(avatar_contradiction_clause,[],[f127275]) ).
fof(f136964,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(sK74)))
| m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),X0,sK75),k1_zfmisc_1(k1_zfmisc_1(sK74))) ),
inference(resolution,[],[f91170,f87403]) ).
fof(f137081,plain,
m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),k1_relset_2(sK74,k1_relset_2(sK74,sK76,sK76),sK76),sK75),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(resolution,[],[f136964,f119003]) ).
fof(f137113,plain,
m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),k1_setfam_1(k2_tarski(sK76,k1_relset_2(sK74,sK76,sK76))),sK75),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(forward_demodulation,[],[f137081,f119101]) ).
fof(f137133,plain,
m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),k1_setfam_1(k2_tarski(sK76,sK76)),sK75),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(forward_demodulation,[],[f137113,f119103]) ).
fof(f137145,plain,
m1_subset_1(k4_subset_1(k1_zfmisc_1(sK74),sK76,sK75),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(forward_demodulation,[],[f137133,f107696]) ).
fof(f137157,plain,
m1_subset_1(k2_xboole_0(sK75,sK76),k1_zfmisc_1(k1_zfmisc_1(sK74))),
inference(forward_demodulation,[],[f137145,f122067]) ).
fof(f137164,plain,
( $false
| spl2393_138 ),
inference(forward_subsumption_resolution,[],[f137157,f122046]) ).
fof(f137165,plain,
spl2393_138,
inference(avatar_contradiction_clause,[],[f137164]) ).
cnf(s102,plain,
( ~ spl2393_138
| ~ spl2393_140 ),
inference(sat_conversion,[],[f120398]) ).
cnf(s170,plain,
spl2393_140,
inference(sat_conversion,[],[f127276]) ).
cnf(s319,plain,
spl2393_138,
inference(sat_conversion,[],[f137165]) ).
cnf(s324,plain,
$false,
inference(rat,[],[s102,s170,s319]) ).
fof(f137175,plain,
$false,
inference(avatar_sat_refutation,[],[s324]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU417+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.10/0.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 28 05:19:39 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 21.02/8.65 % (4179881)Detected formulas, will run a generic FOF schedule.
% 21.02/8.65 % (4179886)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=2730994244:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 21.02/8.65 % (4179887)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=2383392814:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 21.02/8.65 % (4179888)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=3014077625:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 21.02/8.65 % (4179889)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=277731347:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 21.02/8.65 % (4179890)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2348305013:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 21.02/8.65 % (4179892)dis-21_1_sil=8000:lcm=predicate:random_seed=82829522: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)
% 21.02/8.65 % (4179891)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1697564267:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 21.02/8.65 % (4179889)Instruction limit reached!
% 21.02/8.65 % (4179889)------------------------------
% 21.02/8.65 % (4179889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/8.65 % (4179889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/8.65 % (4179889)CaDiCaL version: 2.1.3
% 21.02/8.65 % (4179889)Termination reason: Instruction limit
% 21.02/8.65 % (4179889)Termination phase: SInE selection
% 21.02/8.65 % (4179889)Time elapsed: 0.084 s
% 21.02/8.65 % (4179889)Peak memory usage: 201 MB
% 21.02/8.65 % (4179889)Instructions burned: 109 (million)
% 21.02/8.65 % (4179891)Instruction limit reached!
% 21.02/8.65 % (4179891)------------------------------
% 21.02/8.65 % (4179891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/8.65 % (4179891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/8.65 % (4179891)CaDiCaL version: 2.1.3
% 21.02/8.65 % (4179891)Termination reason: Instruction limit
% 21.02/8.65 % (4179891)Termination phase: Property scanning
% 21.02/8.65 % (4179891)Time elapsed: 0.068 s
% 21.02/8.65 % (4179891)Peak memory usage: 201 MB
% 21.02/8.65 % (4179891)Instructions burned: 140 (million)
% 21.02/8.65 % (4179890)Instruction limit reached!
% 21.02/8.65 % (4179890)------------------------------
% 21.02/8.65 % (4179890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/8.65 % (4179890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/8.65 % (4179890)CaDiCaL version: 2.1.3
% 21.02/8.65 % (4179890)Termination reason: Instruction limit
% 21.02/8.65 % (4179890)Termination phase: SInE selection
% 21.02/8.65 % (4179890)Time elapsed: 0.095 s
% 21.02/8.65 % (4179890)Peak memory usage: 201 MB
% 21.02/8.65 % (4179890)Instructions burned: 119 (million)
% 21.02/8.65 % (4179892)Instruction limit reached!
% 21.02/8.65 % (4179892)------------------------------
% 21.02/8.65 % (4179892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/8.65 % (4179892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/8.65 % (4179892)CaDiCaL version: 2.1.3
% 21.02/8.65 % (4179892)Termination reason: Instruction limit
% 21.02/8.65 % (4179892)Termination phase: SInE selection
% 21.02/8.65 % (4179892)Time elapsed: 0.104 s
% 21.02/8.65 % (4179892)Peak memory usage: 201 MB
% 21.02/8.65 % (4179892)Instructions burned: 130 (million)
% 21.02/8.65 % (4179900)lrs+10_1_sil=8000:sp=occurrence:random_seed=320201991:i=285:sd=3:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/285Mi)
% 21.02/8.65 % (4179902)lrs+1011_1_sil=32000:sp=occurrence:random_seed=466239668:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 21.02/8.65 % (4179901)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2396799554:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/157Mi)
% 21.02/8.65 % (4179903)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=3418297716:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 21.02/8.65 % (4179901)Instruction limit reached!
% 28.65/9.74 % (4179901)------------------------------
% 28.65/9.74 % (4179901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.65/9.74 % (4179901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.65/9.74 % (4179901)CaDiCaL version: 2.1.3
% 28.65/9.74 % (4179901)Termination reason: Instruction limit
% 28.65/9.74 % (4179901)Termination phase: Property scanning
% 28.65/9.74 % (4179901)Time elapsed: 0.077 s
% 28.65/9.74 % (4179901)Peak memory usage: 201 MB
% 28.65/9.74 % (4179901)Instructions burned: 159 (million)
% 28.65/9.74 % (4179903)Instruction limit reached!
% 28.65/9.74 % (4179903)------------------------------
% 28.65/9.74 % (4179903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.65/9.74 % (4179903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.65/9.74 % (4179903)CaDiCaL version: 2.1.3
% 28.65/9.74 % (4179903)Termination reason: Instruction limit
% 28.65/9.74 % (4179903)Termination phase: Property scanning
% 28.65/9.74 % (4179903)Time elapsed: 0.116 s
% 28.65/9.74 % (4179903)Peak memory usage: 201 MB
% 28.65/9.74 % (4179903)Instructions burned: 250 (million)
% 28.65/9.74 % (4179900)Instruction limit reached!
% 28.65/9.74 % (4179900)------------------------------
% 28.65/9.74 % (4179900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.65/9.74 % (4179900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.65/9.74 % (4179900)CaDiCaL version: 2.1.3
% 28.65/9.74 % (4179900)Termination reason: Instruction limit
% 28.65/9.74 % (4179900)Termination phase: SInE selection
% 28.65/9.74 % (4179900)Time elapsed: 0.210 s
% 28.65/9.74 % (4179900)Peak memory usage: 201 MB
% 28.65/9.74 % (4179900)Instructions burned: 289 (million)
% 28.65/9.74 % (4179908)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1646403690:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2939 on theBenchmark for (2939ds/294Mi)
% 28.65/9.74 % (4179902)Instruction limit reached!
% 28.65/9.74 % (4179902)------------------------------
% 28.65/9.74 % (4179902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.65/9.74 % (4179902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.65/9.74 % (4179902)CaDiCaL version: 2.1.3
% 28.65/9.74 % (4179902)Termination reason: Instruction limit
% 28.65/9.74 % (4179902)Termination phase: SInE selection
% 28.65/9.74 % (4179902)Time elapsed: 0.232 s
% 28.65/9.74 % (4179902)Peak memory usage: 201 MB
% 28.65/9.74 % (4179902)Instructions burned: 325 (million)
% 28.65/9.74 % (4179909)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1519966204:i=2350_2938 on theBenchmark for (2938ds/2350Mi)
% 28.65/9.74 % (4179910)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=599633391:cts=off:i=113:fsr=off:ss=included:sgt=4_2938 on theBenchmark for (2938ds/113Mi)
% 28.65/9.74 % (4179912)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4203503500:i=127:av=off:fsr=off:sup=off_2938 on theBenchmark for (2938ds/127Mi)
% 28.65/9.74 % (4179910)Instruction limit reached!
% 28.65/9.74 % (4179910)------------------------------
% 28.65/9.74 % (4179910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.65/9.74 % (4179910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.65/9.74 % (4179910)CaDiCaL version: 2.1.3
% 28.65/9.74 % (4179910)Termination reason: Instruction limit
% 28.65/9.74 % (4179910)Termination phase: SInE selection
% 28.65/9.74 % (4179910)Time elapsed: 0.091 s
% 28.65/9.74 % (4179910)Peak memory usage: 201 MB
% 28.65/9.74 % (4179910)Instructions burned: 113 (million)
% 28.65/9.74 % (4179908)Instruction limit reached!
% 28.65/9.74 % (4179908)------------------------------
% 28.65/9.74 % (4179908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.65/9.74 % (4179908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.65/9.74 % (4179908)CaDiCaL version: 2.1.3
% 28.65/9.74 % (4179908)Termination reason: Instruction limit
% 28.65/9.74 % (4179908)Termination phase: SInE selection
% 28.65/9.74 % (4179908)Time elapsed: 0.230 s
% 28.65/9.74 % (4179908)Peak memory usage: 201 MB
% 28.65/9.74 % (4179908)Instructions burned: 295 (million)
% 28.65/9.74 % (4179912)Instruction limit reached!
% 28.65/9.74 % (4179912)------------------------------
% 28.65/9.74 % (4179912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.65/9.74 % (4179912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.65/9.74 % (4179912)CaDiCaL version: 2.1.3
% 73.38/16.01 % (4179912)Termination reason: Instruction limit
% 73.38/16.01 % (4179912)Termination phase: Preprocessing 1
% 73.38/16.01 % (4179912)Time elapsed: 0.101 s
% 73.38/16.01 % (4179912)Peak memory usage: 202 MB
% 73.38/16.01 % (4179912)Instructions burned: 128 (million)
% 73.38/16.01 % (4179916)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=685591895:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2935 on theBenchmark for (2935ds/114Mi)
% 73.38/16.01 % (4179917)lrs+10_1_sil=8000:sp=occurrence:random_seed=548397313:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2935 on theBenchmark for (2935ds/907Mi)
% 73.38/16.01 % (4179918)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=222835366:i=437:sd=1:aac=none:ss=included_2935 on theBenchmark for (2935ds/437Mi)
% 73.38/16.01 % (4179916)Instruction limit reached!
% 73.38/16.01 % (4179916)------------------------------
% 73.38/16.01 % (4179916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.38/16.01 % (4179916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.38/16.01 % (4179916)CaDiCaL version: 2.1.3
% 73.38/16.01 % (4179916)Termination reason: Instruction limit
% 73.38/16.01 % (4179916)Termination phase: Property scanning
% 73.38/16.01 % (4179916)Time elapsed: 0.059 s
% 73.38/16.01 % (4179916)Peak memory usage: 201 MB
% 73.38/16.01 % (4179916)Instructions burned: 116 (million)
% 73.38/16.01 % (4179922)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2239024326:i=5202:ss=axioms:sgt=16_2933 on theBenchmark for (2933ds/5202Mi)
% 73.38/16.01 % (4179918)Instruction limit reached!
% 73.38/16.01 % (4179918)------------------------------
% 73.38/16.01 % (4179918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.38/16.01 % (4179918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.38/16.01 % (4179918)CaDiCaL version: 2.1.3
% 73.38/16.01 % (4179918)Termination reason: Instruction limit
% 73.38/16.01 % (4179918)Termination phase: SInE selection
% 73.38/16.01 % (4179918)Time elapsed: 0.323 s
% 73.38/16.01 % (4179918)Peak memory usage: 202 MB
% 73.38/16.01 % (4179918)Instructions burned: 438 (million)
% 73.38/16.01 % (4179924)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=367516465:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2931 on theBenchmark for (2931ds/134Mi)
% 73.38/16.01 % (4179924)Instruction limit reached!
% 73.38/16.01 % (4179924)------------------------------
% 73.38/16.01 % (4179924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.38/16.01 % (4179924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.38/16.01 % (4179924)CaDiCaL version: 2.1.3
% 73.38/16.01 % (4179924)Termination reason: Instruction limit
% 73.38/16.01 % (4179924)Termination phase: SInE selection
% 73.38/16.01 % (4179924)Time elapsed: 0.103 s
% 73.38/16.01 % (4179924)Peak memory usage: 201 MB
% 73.38/16.01 % (4179924)Instructions burned: 134 (million)
% 73.38/16.01 % (4179917)Instruction limit reached!
% 73.38/16.01 % (4179917)------------------------------
% 73.38/16.01 % (4179917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.38/16.01 % (4179917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.38/16.01 % (4179917)CaDiCaL version: 2.1.3
% 73.38/16.01 % (4179917)Termination reason: Instruction limit
% 73.38/16.01 % (4179917)Termination phase: Preprocessing 1
% 73.38/16.01 % (4179917)Time elapsed: 0.679 s
% 73.38/16.01 % (4179917)Peak memory usage: 204 MB
% 73.38/16.01 % (4179917)Instructions burned: 907 (million)
% 73.38/16.01 % (4179926)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1091990085:st=8:i=592:sd=3:ep=RST:ss=axioms_2928 on theBenchmark for (2928ds/592Mi)
% 73.38/16.01 % (4179927)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=765014777:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 73.38/16.01 % (4179926)Instruction limit reached!
% 73.38/16.01 % (4179926)------------------------------
% 73.38/16.01 % (4179926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.38/16.01 % (4179926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.38/16.01 % (4179926)CaDiCaL version: 2.1.3
% 73.38/16.01 % (4179926)Termination reason: Instruction limit
% 73.38/16.01 % (4179926)Termination phase: SInE selection
% 73.38/16.01 % (4179926)Time elapsed: 0.386 s
% 73.38/16.01 % (4179926)Peak memory usage: 203 MB
% 73.38/16.01 % (4179926)Instructions burned: 593 (million)
% 73.38/16.01 % (4179930)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=4146780613:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2923 on theBenchmark for (2923ds/125Mi)
% 57.67/16.57 % (4179930)Instruction limit reached!
% 57.67/16.57 % (4179930)------------------------------
% 57.67/16.57 % (4179930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179930)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179930)Termination reason: Instruction limit
% 57.67/16.57 % (4179930)Termination phase: Property scanning
% 57.67/16.57 % (4179930)Time elapsed: 0.063 s
% 57.67/16.57 % (4179930)Peak memory usage: 201 MB
% 57.67/16.57 % (4179930)Instructions burned: 126 (million)
% 57.67/16.57 % (4179932)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1203304846:i=134:gtgl=5:slsql=off:gtg=exists_sym_2921 on theBenchmark for (2921ds/134Mi)
% 57.67/16.57 % (4179932)Instruction limit reached!
% 57.67/16.57 % (4179932)------------------------------
% 57.67/16.57 % (4179932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179932)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179932)Termination reason: Instruction limit
% 57.67/16.57 % (4179932)Termination phase: Property scanning
% 57.67/16.57 % (4179932)Time elapsed: 0.066 s
% 57.67/16.57 % (4179932)Peak memory usage: 201 MB
% 57.67/16.57 % (4179932)Instructions burned: 136 (million)
% 57.67/16.57 % (4179909)Instruction limit reached!
% 57.67/16.57 % (4179909)------------------------------
% 57.67/16.57 % (4179909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179909)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179909)Termination reason: Instruction limit
% 57.67/16.57 % (4179909)Termination phase: Preprocessing 3
% 57.67/16.57 % (4179909)Time elapsed: 1.857 s
% 57.67/16.57 % (4179909)Peak memory usage: 304 MB
% 57.67/16.57 % (4179909)Instructions burned: 2351 (million)
% 57.67/16.57 % (4179934)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2620653289:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2919 on theBenchmark for (2919ds/141Mi)
% 57.67/16.57 % (4179935)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1450118451:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2918 on theBenchmark for (2918ds/431Mi)
% 57.67/16.57 % (4179934)Instruction limit reached!
% 57.67/16.57 % (4179934)------------------------------
% 57.67/16.57 % (4179934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179934)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179934)Termination reason: Instruction limit
% 57.67/16.57 % (4179934)Termination phase: SInE selection
% 57.67/16.57 % (4179934)Time elapsed: 0.109 s
% 57.67/16.57 % (4179934)Peak memory usage: 201 MB
% 57.67/16.57 % (4179934)Instructions burned: 141 (million)
% 57.67/16.57 % (4179938)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=1591636021:i=6060:aac=none:ins=25_2916 on theBenchmark for (2916ds/6060Mi)
% 57.67/16.57 % (4179935)Instruction limit reached!
% 57.67/16.57 % (4179935)------------------------------
% 57.67/16.57 % (4179935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179935)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179935)Termination reason: Instruction limit
% 57.67/16.57 % (4179935)Termination phase: SInE selection
% 57.67/16.57 % (4179935)Time elapsed: 0.331 s
% 57.67/16.57 % (4179935)Peak memory usage: 202 MB
% 57.67/16.57 % (4179935)Instructions burned: 432 (million)
% 57.67/16.57 % (4179940)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=2702283102:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2913 on theBenchmark for (2913ds/150Mi)
% 57.67/16.57 % (4179940)Instruction limit reached!
% 57.67/16.57 % (4179940)------------------------------
% 57.67/16.57 % (4179940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179940)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179940)Termination reason: Instruction limit
% 57.67/16.57 % (4179940)Termination phase: SInE selection
% 57.67/16.57 % (4179940)Time elapsed: 0.121 s
% 57.67/16.57 % (4179940)Peak memory usage: 201 MB
% 57.67/16.57 % (4179940)Instructions burned: 150 (million)
% 57.67/16.57 % (4179942)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4008458191:i=14155:bd=all_2911 on theBenchmark for (2911ds/14155Mi)
% 57.67/16.57 % (4179922)Instruction limit reached!
% 57.67/16.57 % (4179922)------------------------------
% 57.67/16.57 % (4179922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179922)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179922)Termination reason: Instruction limit
% 57.67/16.57 % (4179922)Termination phase: Saturation
% 57.67/16.57 % (4179922)Time elapsed: 3.633 s
% 57.67/16.57 % (4179922)Peak memory usage: 364 MB
% 57.67/16.57 % (4179922)Instructions burned: 5202 (million)
% 57.67/16.57 % (4179944)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=598544544:i=667:av=off:fsr=off_2895 on theBenchmark for (2895ds/667Mi)
% 57.67/16.57 % (4179944)Instruction limit reached!
% 57.67/16.57 % (4179944)------------------------------
% 57.67/16.57 % (4179944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179944)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179944)Termination reason: Instruction limit
% 57.67/16.57 % (4179944)Termination phase: Preprocessing 2
% 57.67/16.57 % (4179944)Time elapsed: 0.642 s
% 57.67/16.57 % (4179944)Peak memory usage: 218 MB
% 57.67/16.57 % (4179944)Instructions burned: 668 (million)
% 57.67/16.57 % (4179946)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=1685282920:s2a=on:i=185:s2at=1.8:fdi=4_2887 on theBenchmark for (2887ds/185Mi)
% 57.67/16.57 % (4179946)Instruction limit reached!
% 57.67/16.57 % (4179946)------------------------------
% 57.67/16.57 % (4179946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179946)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179946)Termination reason: Instruction limit
% 57.67/16.57 % (4179946)Termination phase: SInE selection
% 57.67/16.57 % (4179946)Time elapsed: 0.149 s
% 57.67/16.57 % (4179946)Peak memory usage: 201 MB
% 57.67/16.57 % (4179946)Instructions burned: 185 (million)
% 57.67/16.57 % (4179948)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4030639569:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2884 on theBenchmark for (2884ds/193Mi)
% 57.67/16.57 % (4179948)Instruction limit reached!
% 57.67/16.57 % (4179948)------------------------------
% 57.67/16.57 % (4179948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179948)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179948)Termination reason: Instruction limit
% 57.67/16.57 % (4179948)Termination phase: SInE selection
% 57.67/16.57 % (4179948)Time elapsed: 0.154 s
% 57.67/16.57 % (4179948)Peak memory usage: 201 MB
% 57.67/16.57 % (4179948)Instructions burned: 194 (million)
% 57.67/16.57 % (4179950)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1131740372:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2881 on theBenchmark for (2881ds/4850Mi)
% 57.67/16.57 % (4179938)Instruction limit reached!
% 57.67/16.57 % (4179938)------------------------------
% 57.67/16.57 % (4179938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179938)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179938)Termination reason: Instruction limit
% 57.67/16.57 % (4179938)Termination phase: NewCNF
% 57.67/16.57 % (4179938)Time elapsed: 4.855 s
% 57.67/16.57 % (4179938)Peak memory usage: 381 MB
% 57.67/16.57 % (4179938)Instructions burned: 6060 (million)
% 57.67/16.57 % (4179952)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3093084032:i=12111:sd=1:ss=included_2866 on theBenchmark for (2866ds/12111Mi)
% 57.67/16.57 % (4179927)Instruction limit reached!
% 57.67/16.57 % (4179927)------------------------------
% 57.67/16.57 % (4179927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179927)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179927)Termination reason: Instruction limit
% 57.67/16.57 % (4179927)Termination phase: Saturation
% 57.67/16.57 % (4179927)Time elapsed: 7.790 s
% 57.67/16.57 % (4179927)Peak memory usage: 434 MB
% 57.67/16.57 % (4179927)Instructions burned: 13194 (million)
% 57.67/16.57 % (4179887)First to succeed.
% 57.67/16.57 % (4179887)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4179881"
% 57.67/16.57 % (4179955)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3747543343:i=319:kws=precedence:fsr=off_2847 on theBenchmark for (2847ds/319Mi)
% 57.67/16.57 % (4179950)Instruction limit reached!
% 57.67/16.57 % (4179950)------------------------------
% 57.67/16.57 % (4179950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/16.57 % (4179950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/16.57 % (4179950)CaDiCaL version: 2.1.3
% 57.67/16.57 % (4179950)Termination reason: Instruction limit
% 57.67/16.57 % (4179950)Termination phase: Property scanning
% 57.67/16.57 % (4179950)Time elapsed: 3.387 s
% 57.67/16.57 % (4179950)Peak memory usage: 347 MB
% 57.67/16.57 % (4179950)Instructions burned: 4852 (million)
% 57.67/16.57 % (4179957)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3338625084:i=2064:ep=RST_2845 on theBenchmark for (2845ds/2064Mi)
% 57.67/16.57 % (4179887)Refutation found. Thanks to Tanya!
% 57.67/16.57 % SZS status Theorem for theBenchmark
% 57.67/16.57 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/16.82 % (4179887)------------------------------
% 0.17/16.82 % (4179887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/16.82 % (4179887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/16.82 % (4179887)CaDiCaL version: 2.1.3
% 0.17/16.82 % (4179887)Termination reason: Refutation
% 0.17/16.82 % (4179887)Time elapsed: 9.515 s
% 0.17/16.82 % (4179887)Peak memory usage: 494 MB
% 0.17/16.82 % (4179887)Instructions burned: 15713 (million)
% 0.17/16.82 % (4179887)------------------------------
% 0.17/16.82 % (4179887)------------------------------
% 0.17/16.82 % (4179881)Success in time 15.718 s
% 0.17/16.82 % Vampire exiting
%------------------------------------------------------------------------------