%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU438+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:04 PM UTC 2026
% Result : Theorem 12.61s 5.05s
% Output : Refutation 28.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 9
% Syntax : Number of formulae : 76 ( 26 unt; 0 def)
% Number of atoms : 183 ( 20 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 199 ( 92 ~; 81 |; 11 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-4 aty)
% Number of variables : 124 ( 119 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
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(f76,axiom,
! [X0,X1] : r1_tarski(X0,k2_xboole_0(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_xboole_1) ).
fof(f77,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X0,X1)
& r1_tarski(X2,X1) )
=> r1_tarski(k2_xboole_0(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_xboole_1) ).
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(f19064,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_relset_2) ).
fof(f19065,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> k8_relset_2(X0,X1,X2,X3) = k7_relset_2(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_relset_2) ).
fof(f19111,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( r1_tarski(X3,X4)
=> r1_tarski(k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t40_relset_2) ).
fof(f19112,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> r1_tarski(k4_subset_1(X1,k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4)),k8_relset_2(X0,X1,X2,k4_subset_1(k2_zfmisc_1(X0,X1),X3,X4))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_relset_2) ).
fof(f19113,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> r1_tarski(k4_subset_1(X1,k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4)),k8_relset_2(X0,X1,X2,k4_subset_1(k2_zfmisc_1(X0,X1),X3,X4))) ) ) ),
inference(negated_conjecture,[status(cth)],[f19112]) ).
fof(f19167,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f19064]) ).
fof(f19168,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(flattening,[],[f19167]) ).
fof(f19169,plain,
! [X0,X1,X2,X3] :
( k8_relset_2(X0,X1,X2,X3) = k7_relset_2(X0,X1,X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f19065]) ).
fof(f19170,plain,
! [X0,X1,X2,X3] :
( k8_relset_2(X0,X1,X2,X3) = k7_relset_2(X0,X1,X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(flattening,[],[f19169]) ).
fof(f19222,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( r1_tarski(k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4))
| ~ r1_tarski(X3,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19111]) ).
fof(f19223,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( r1_tarski(k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4))
| ~ r1_tarski(X3,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19222]) ).
fof(f19224,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( ~ r1_tarski(k4_subset_1(X1,k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4)),k8_relset_2(X0,X1,X2,k4_subset_1(k2_zfmisc_1(X0,X1),X3,X4)))
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19113]) ).
fof(f19483,plain,
! [X0,X1,X2] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(ennf_transformation,[],[f77]) ).
fof(f19484,plain,
! [X0,X1,X2] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(flattening,[],[f19483]) ).
fof(f19811,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(f19812,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,[],[f19811]) ).
fof(f19817,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(f19818,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,[],[f19817]) ).
fof(f21833,plain,
( ~ r1_tarski(k4_subset_1(sK19,k8_relset_2(sK18,sK19,sK20,sK21),k8_relset_2(sK18,sK19,sK20,sK22)),k8_relset_2(sK18,sK19,sK20,k4_subset_1(k2_zfmisc_1(sK18,sK19),sK21,sK22)))
& m1_subset_1(sK22,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
& m1_subset_1(sK21,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
& m1_subset_1(sK20,k1_zfmisc_1(sK18)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20,sK21,sK22]),skolemize(X0,sK18),skolemize(X1,sK19),skolemize(X2,sK20),skolemize(X3,sK21),skolemize(X4,sK22)],[f19224]) ).
fof(f22761,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19168]) ).
fof(f22762,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| k8_relset_2(X0,X1,X2,X3) = k7_relset_2(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f19170]) ).
fof(f22823,plain,
! [X2,X3,X0,X1,X4] :
( r1_tarski(k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4))
| ~ r1_tarski(X3,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19223]) ).
fof(f22824,plain,
m1_subset_1(sK20,k1_zfmisc_1(sK18)),
inference(cnf_transformation,[],[f21833]) ).
fof(f22825,plain,
m1_subset_1(sK21,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))),
inference(cnf_transformation,[],[f21833]) ).
fof(f22826,plain,
m1_subset_1(sK22,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))),
inference(cnf_transformation,[],[f21833]) ).
fof(f22827,plain,
~ r1_tarski(k4_subset_1(sK19,k8_relset_2(sK18,sK19,sK20,sK21),k8_relset_2(sK18,sK19,sK20,sK22)),k8_relset_2(sK18,sK19,sK20,k4_subset_1(k2_zfmisc_1(sK18,sK19),sK21,sK22))),
inference(cnf_transformation,[],[f21833]) ).
fof(f23182,plain,
! [X2,X0,X1] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(cnf_transformation,[],[f19484]) ).
fof(f23183,plain,
! [X0,X1] : r1_tarski(X0,k2_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f76]) ).
fof(f23189,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
inference(cnf_transformation,[],[f54]) ).
fof(f23789,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,[],[f19812]) ).
fof(f23792,plain,
! [X2,X0,X1] :
( 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(cnf_transformation,[],[f19818]) ).
fof(f28729,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| k4_subset_1(k2_zfmisc_1(sK18,sK19),X0,sK22) = k2_xboole_0(X0,sK22) ),
inference(resolution,[],[f23789,f22826]) ).
fof(f28741,plain,
k4_subset_1(k2_zfmisc_1(sK18,sK19),sK21,sK22) = k2_xboole_0(sK21,sK22),
inference(resolution,[],[f28729,f22825]) ).
fof(f28746,plain,
~ r1_tarski(k4_subset_1(sK19,k8_relset_2(sK18,sK19,sK20,sK21),k8_relset_2(sK18,sK19,sK20,sK22)),k8_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))),
inference(superposition,[],[f22827,f28741]) ).
fof(f28747,plain,
( m1_subset_1(k2_xboole_0(sK21,sK22),k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK21,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK22,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(superposition,[],[f23792,f28741]) ).
fof(f28748,plain,
( m1_subset_1(k2_xboole_0(sK21,sK22),k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK22,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(forward_subsumption_resolution,[],[f28747,f22825]) ).
fof(f28749,plain,
m1_subset_1(k2_xboole_0(sK21,sK22),k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))),
inference(forward_subsumption_resolution,[],[f28748,f22826]) ).
fof(f28786,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK18))
| k8_relset_2(sK18,sK19,X0,k2_xboole_0(sK21,sK22)) = k7_relset_2(sK18,sK19,X0,k2_xboole_0(sK21,sK22)) ),
inference(resolution,[],[f22762,f28749]) ).
fof(f28789,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK18))
| k8_relset_2(sK18,sK19,X0,sK21) = k7_relset_2(sK18,sK19,X0,sK21) ),
inference(resolution,[],[f22762,f22825]) ).
fof(f28790,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK18))
| k8_relset_2(sK18,sK19,X0,sK22) = k7_relset_2(sK18,sK19,X0,sK22) ),
inference(resolution,[],[f22762,f22826]) ).
fof(f28793,plain,
k8_relset_2(sK18,sK19,sK20,sK22) = k7_relset_2(sK18,sK19,sK20,sK22),
inference(resolution,[],[f28790,f22824]) ).
fof(f28797,plain,
! [X0] :
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK22),k8_relset_2(sK18,sK19,sK20,X0))
| ~ r1_tarski(sK22,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK22,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK20,k1_zfmisc_1(sK18)) ),
inference(superposition,[],[f22823,f28793]) ).
fof(f28800,plain,
( m1_subset_1(k7_relset_2(sK18,sK19,sK20,sK22),k1_zfmisc_1(sK19))
| ~ m1_subset_1(sK20,k1_zfmisc_1(sK18))
| ~ m1_subset_1(sK22,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(superposition,[],[f22761,f28793]) ).
fof(f28801,plain,
( m1_subset_1(k7_relset_2(sK18,sK19,sK20,sK22),k1_zfmisc_1(sK19))
| ~ m1_subset_1(sK22,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(forward_subsumption_resolution,[],[f28800,f22824]) ).
fof(f28804,plain,
! [X0] :
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK22),k8_relset_2(sK18,sK19,sK20,X0))
| ~ r1_tarski(sK22,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK20,k1_zfmisc_1(sK18)) ),
inference(forward_subsumption_resolution,[],[f28797,f22826]) ).
fof(f28807,plain,
m1_subset_1(k7_relset_2(sK18,sK19,sK20,sK22),k1_zfmisc_1(sK19)),
inference(forward_subsumption_resolution,[],[f28801,f22826]) ).
fof(f28810,plain,
! [X0] :
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK22),k8_relset_2(sK18,sK19,sK20,X0))
| ~ r1_tarski(sK22,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(forward_subsumption_resolution,[],[f28804,f22824]) ).
fof(f28814,plain,
k8_relset_2(sK18,sK19,sK20,sK21) = k7_relset_2(sK18,sK19,sK20,sK21),
inference(resolution,[],[f28789,f22824]) ).
fof(f28815,plain,
~ r1_tarski(k4_subset_1(sK19,k7_relset_2(sK18,sK19,sK20,sK21),k8_relset_2(sK18,sK19,sK20,sK22)),k8_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))),
inference(superposition,[],[f28746,f28814]) ).
fof(f28818,plain,
! [X0] :
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK21),k8_relset_2(sK18,sK19,sK20,X0))
| ~ r1_tarski(sK21,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK21,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK20,k1_zfmisc_1(sK18)) ),
inference(superposition,[],[f22823,f28814]) ).
fof(f28821,plain,
( m1_subset_1(k7_relset_2(sK18,sK19,sK20,sK21),k1_zfmisc_1(sK19))
| ~ m1_subset_1(sK20,k1_zfmisc_1(sK18))
| ~ m1_subset_1(sK21,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(superposition,[],[f22761,f28814]) ).
fof(f28822,plain,
( m1_subset_1(k7_relset_2(sK18,sK19,sK20,sK21),k1_zfmisc_1(sK19))
| ~ m1_subset_1(sK21,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(forward_subsumption_resolution,[],[f28821,f22824]) ).
fof(f28825,plain,
! [X0] :
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK21),k8_relset_2(sK18,sK19,sK20,X0))
| ~ r1_tarski(sK21,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19)))
| ~ m1_subset_1(sK20,k1_zfmisc_1(sK18)) ),
inference(forward_subsumption_resolution,[],[f28818,f22825]) ).
fof(f28828,plain,
~ r1_tarski(k4_subset_1(sK19,k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,sK22)),k8_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))),
inference(forward_demodulation,[],[f28815,f28793]) ).
fof(f28829,plain,
m1_subset_1(k7_relset_2(sK18,sK19,sK20,sK21),k1_zfmisc_1(sK19)),
inference(forward_subsumption_resolution,[],[f28822,f22825]) ).
fof(f28832,plain,
! [X0] :
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK21),k8_relset_2(sK18,sK19,sK20,X0))
| ~ r1_tarski(sK21,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(forward_subsumption_resolution,[],[f28825,f22824]) ).
fof(f28842,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK19))
| k2_xboole_0(X0,k7_relset_2(sK18,sK19,sK20,sK22)) = k4_subset_1(sK19,X0,k7_relset_2(sK18,sK19,sK20,sK22)) ),
inference(resolution,[],[f28807,f23789]) ).
fof(f29503,plain,
k4_subset_1(sK19,k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,sK22)) = k2_xboole_0(k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,sK22)),
inference(resolution,[],[f28842,f28829]) ).
fof(f29629,plain,
! [X0,X1] : r1_tarski(X1,k2_xboole_0(X0,X1)),
inference(superposition,[],[f23183,f23189]) ).
fof(f32174,plain,
k8_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22)) = k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22)),
inference(resolution,[],[f28786,f22824]) ).
fof(f32178,plain,
~ r1_tarski(k4_subset_1(sK19,k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,sK22)),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))),
inference(superposition,[],[f28828,f32174]) ).
fof(f32185,plain,
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK22),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22)))
| ~ r1_tarski(sK22,k2_xboole_0(sK21,sK22))
| ~ m1_subset_1(k2_xboole_0(sK21,sK22),k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(superposition,[],[f28810,f32174]) ).
fof(f32186,plain,
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22)))
| ~ r1_tarski(sK21,k2_xboole_0(sK21,sK22))
| ~ m1_subset_1(k2_xboole_0(sK21,sK22),k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(superposition,[],[f28832,f32174]) ).
fof(f32205,plain,
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22)))
| ~ m1_subset_1(k2_xboole_0(sK21,sK22),k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(forward_subsumption_resolution,[],[f32186,f23183]) ).
fof(f32206,plain,
( r1_tarski(k7_relset_2(sK18,sK19,sK20,sK22),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22)))
| ~ m1_subset_1(k2_xboole_0(sK21,sK22),k1_zfmisc_1(k2_zfmisc_1(sK18,sK19))) ),
inference(forward_subsumption_resolution,[],[f32185,f29629]) ).
fof(f32207,plain,
~ r1_tarski(k2_xboole_0(k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,sK22)),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))),
inference(forward_demodulation,[],[f32178,f29503]) ).
fof(f32218,plain,
r1_tarski(k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))),
inference(forward_subsumption_resolution,[],[f32205,f28749]) ).
fof(f32219,plain,
r1_tarski(k7_relset_2(sK18,sK19,sK20,sK22),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))),
inference(forward_subsumption_resolution,[],[f32206,f28749]) ).
fof(f50532,plain,
( ~ r1_tarski(k7_relset_2(sK18,sK19,sK20,sK21),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22)))
| ~ r1_tarski(k7_relset_2(sK18,sK19,sK20,sK22),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))) ),
inference(resolution,[],[f32207,f23182]) ).
fof(f50533,plain,
~ r1_tarski(k7_relset_2(sK18,sK19,sK20,sK22),k7_relset_2(sK18,sK19,sK20,k2_xboole_0(sK21,sK22))),
inference(forward_subsumption_resolution,[],[f50532,f32218]) ).
fof(f50534,plain,
$false,
inference(forward_subsumption_resolution,[],[f50533,f32219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU438+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n004.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:28:39 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.41 Running first-order theorem proving
% 0.11/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
% 12.02/2.91 % (30561)Detected formulas, will run a generic FOF schedule.
% 12.02/2.91 % (30571)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4089204180:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 12.02/2.91 % (30566)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=3834538494:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 12.02/2.91 % (30568)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=1817416181:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 12.02/2.91 % (30570)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=250329126:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 12.02/2.91 % (30569)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2560338074:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 12.02/2.91 % (30572)dis-21_1_sil=8000:lcm=predicate:random_seed=1893674875:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 12.02/2.91 % (30567)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=2367502446:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 12.02/2.91 % (30571)Instruction limit reached!
% 12.02/2.91 % (30571)------------------------------
% 12.02/2.91 % (30571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.91 % (30571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.91 % (30571)CaDiCaL version: 2.1.3
% 12.02/2.91 % (30571)Termination reason: Instruction limit
% 12.02/2.91 % (30571)Termination phase: Property scanning
% 12.02/2.91 % (30571)Time elapsed: 0.059 s
% 12.02/2.91 % (30571)Peak memory usage: 112 MB
% 12.02/2.91 % (30571)Instructions burned: 141 (million)
% 12.02/2.91 % (30569)Instruction limit reached!
% 12.02/2.91 % (30569)------------------------------
% 12.02/2.91 % (30569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.91 % (30569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.92 % (30569)CaDiCaL version: 2.1.3
% 12.02/2.92 % (30569)Termination reason: Instruction limit
% 12.02/2.92 % (30569)Termination phase: SInE selection
% 12.02/2.92 % (30569)Time elapsed: 0.083 s
% 12.02/2.92 % (30569)Peak memory usage: 112 MB
% 12.02/2.92 % (30569)Instructions burned: 110 (million)
% 12.02/2.92 % (30570)Instruction limit reached!
% 12.02/2.92 % (30570)------------------------------
% 12.02/2.92 % (30570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.92 % (30570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.92 % (30570)CaDiCaL version: 2.1.3
% 12.02/2.92 % (30570)Termination reason: Instruction limit
% 12.02/2.92 % (30570)Termination phase: Preprocessing 1
% 12.02/2.92 % (30570)Time elapsed: 0.098 s
% 12.02/2.92 % (30570)Peak memory usage: 113 MB
% 12.02/2.92 % (30570)Instructions burned: 119 (million)
% 12.02/2.92 % (30572)Instruction limit reached!
% 12.02/2.92 % (30572)------------------------------
% 12.02/2.92 % (30572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.92 % (30572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.92 % (30572)CaDiCaL version: 2.1.3
% 12.02/2.92 % (30572)Termination reason: Instruction limit
% 12.02/2.92 % (30572)Termination phase: SInE selection
% 12.02/2.92 % (30572)Time elapsed: 0.107 s
% 12.02/2.92 % (30572)Peak memory usage: 112 MB
% 12.02/2.92 % (30572)Instructions burned: 129 (million)
% 12.02/2.92 % (30580)lrs+10_1_sil=8000:sp=occurrence:random_seed=2521713526:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 12.02/2.92 % (30581)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3382258205:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 12.02/2.92 % (30582)lrs+1011_1_sil=32000:sp=occurrence:random_seed=277944214:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi)
% 12.02/2.92 % (30583)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=1847957849:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 12.02/2.92 % (30581)Instruction limit reached!
% 12.02/2.92 % (30581)------------------------------
% 12.02/2.92 % (30581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30581)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30581)Termination reason: Instruction limit
% 12.61/5.05 % (30581)Termination phase: Property scanning
% 12.61/5.05 % (30581)Time elapsed: 0.069 s
% 12.61/5.05 % (30581)Peak memory usage: 112 MB
% 12.61/5.05 % (30581)Instructions burned: 158 (million)
% 12.61/5.05 % (30583)Instruction limit reached!
% 12.61/5.05 % (30583)------------------------------
% 12.61/5.05 % (30583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30583)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30583)Termination reason: Instruction limit
% 12.61/5.05 % (30583)Termination phase: Property scanning
% 12.61/5.05 % (30583)Time elapsed: 0.067 s
% 12.61/5.05 % (30583)Peak memory usage: 113 MB
% 12.61/5.05 % (30583)Instructions burned: 248 (million)
% 12.61/5.05 % (30580)Instruction limit reached!
% 12.61/5.05 % (30580)------------------------------
% 12.61/5.05 % (30580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30580)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30580)Termination reason: Instruction limit
% 12.61/5.05 % (30580)Termination phase: Saturation
% 12.61/5.05 % (30580)Time elapsed: 0.202 s
% 12.61/5.05 % (30580)Peak memory usage: 120 MB
% 12.61/5.05 % (30580)Instructions burned: 285 (million)
% 12.61/5.05 % (30589)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3495361941:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 12.61/5.05 % (30588)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2222392966:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 12.61/5.05 % (30582)Instruction limit reached!
% 12.61/5.05 % (30582)------------------------------
% 12.61/5.05 % (30582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30582)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30582)Termination reason: Instruction limit
% 12.61/5.05 % (30582)Termination phase: Saturation
% 12.61/5.05 % (30582)Time elapsed: 0.249 s
% 12.61/5.05 % (30582)Peak memory usage: 120 MB
% 12.61/5.05 % (30582)Instructions burned: 326 (million)
% 12.61/5.05 % (30590)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3851866813:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 12.61/5.05 % (30588)Instruction limit reached!
% 12.61/5.05 % (30588)------------------------------
% 12.61/5.05 % (30588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30588)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30588)Termination reason: Instruction limit
% 12.61/5.05 % (30588)Termination phase: Property scanning
% 12.61/5.05 % (30588)Time elapsed: 0.205 s
% 12.61/5.05 % (30588)Peak memory usage: 118 MB
% 12.61/5.05 % (30588)Instructions burned: 295 (million)
% 12.61/5.05 % (30593)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2712726656:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 12.61/5.05 % (30590)Instruction limit reached!
% 12.61/5.05 % (30590)------------------------------
% 12.61/5.05 % (30590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30590)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30590)Termination reason: Instruction limit
% 12.61/5.05 % (30590)Termination phase: SInE selection
% 12.61/5.05 % (30590)Time elapsed: 0.092 s
% 12.61/5.05 % (30590)Peak memory usage: 112 MB
% 12.61/5.05 % (30590)Instructions burned: 113 (million)
% 12.61/5.05 % (30593)Instruction limit reached!
% 12.61/5.05 % (30593)------------------------------
% 12.61/5.05 % (30593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30593)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30593)Termination reason: Instruction limit
% 12.61/5.05 % (30593)Termination phase: Preprocessing 1
% 12.61/5.05 % (30593)Time elapsed: 0.091 s
% 12.61/5.05 % (30593)Peak memory usage: 113 MB
% 12.61/5.05 % (30593)Instructions burned: 128 (million)
% 12.61/5.05 % (30595)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3795796352:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 12.61/5.05 % (30597)lrs+10_1_sil=8000:sp=occurrence:random_seed=2028284487:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 12.61/5.05 % (30595)Instruction limit reached!
% 12.61/5.05 % (30595)------------------------------
% 12.61/5.05 % (30595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30595)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30595)Termination reason: Instruction limit
% 12.61/5.05 % (30595)Termination phase: Property scanning
% 12.61/5.05 % (30595)Time elapsed: 0.050 s
% 12.61/5.05 % (30595)Peak memory usage: 112 MB
% 12.61/5.05 % (30595)Instructions burned: 115 (million)
% 12.61/5.05 % (30598)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2993969206:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 12.61/5.05 % (30601)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1173688653:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 12.61/5.05 % (30589)Instruction limit reached!
% 12.61/5.05 % (30589)------------------------------
% 12.61/5.05 % (30589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30589)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30589)Termination reason: Instruction limit
% 12.61/5.05 % (30589)Termination phase: Property scanning
% 12.61/5.05 % (30589)Time elapsed: 0.731 s
% 12.61/5.05 % (30589)Peak memory usage: 171 MB
% 12.61/5.05 % (30589)Instructions burned: 2350 (million)
% 12.61/5.05 % (30598)Instruction limit reached!
% 12.61/5.05 % (30598)------------------------------
% 12.61/5.05 % (30598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30598)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30598)Termination reason: Instruction limit
% 12.61/5.05 % (30598)Termination phase: Saturation
% 12.61/5.05 % (30598)Time elapsed: 0.306 s
% 12.61/5.05 % (30598)Peak memory usage: 121 MB
% 12.61/5.05 % (30598)Instructions burned: 438 (million)
% 12.61/5.05 % (30604)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3505305035:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 12.61/5.05 % (30605)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4196438646:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 12.61/5.05 % (30597)Instruction limit reached!
% 12.61/5.05 % (30597)------------------------------
% 12.61/5.05 % (30597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30597)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30597)Termination reason: Instruction limit
% 12.61/5.05 % (30597)Termination phase: Saturation
% 12.61/5.05 % (30597)Time elapsed: 0.627 s
% 12.61/5.05 % (30597)Peak memory usage: 128 MB
% 12.61/5.05 % (30597)Instructions burned: 907 (million)
% 12.61/5.05 % (30604)Instruction limit reached!
% 12.61/5.05 % (30604)------------------------------
% 12.61/5.05 % (30604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30604)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30604)Termination reason: Instruction limit
% 12.61/5.05 % (30604)Termination phase: NewCNF
% 12.61/5.05 % (30604)Time elapsed: 0.118 s
% 12.61/5.05 % (30604)Peak memory usage: 115 MB
% 12.61/5.05 % (30604)Instructions burned: 134 (million)
% 12.61/5.05 % (30608)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3573141593:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 12.61/5.05 % (30609)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=348480674:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 12.61/5.05 % (30609)Instruction limit reached!
% 12.61/5.05 % (30609)------------------------------
% 12.61/5.05 % (30609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30609)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30609)Termination reason: Instruction limit
% 12.61/5.05 % (30609)Termination phase: Property scanning
% 12.61/5.05 % (30609)Time elapsed: 0.054 s
% 12.61/5.05 % (30609)Peak memory usage: 112 MB
% 12.61/5.05 % (30609)Instructions burned: 127 (million)
% 12.61/5.05 % (30605)Instruction limit reached!
% 12.61/5.05 % (30605)------------------------------
% 12.61/5.05 % (30605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30605)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30605)Termination reason: Instruction limit
% 12.61/5.05 % (30605)Termination phase: Preprocessing 3
% 12.61/5.05 % (30605)Time elapsed: 0.442 s
% 12.61/5.05 % (30605)Peak memory usage: 134 MB
% 12.61/5.05 % (30605)Instructions burned: 592 (million)
% 12.61/5.05 % (30612)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=720220357:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 12.61/5.05 % (30612)Instruction limit reached!
% 12.61/5.05 % (30612)------------------------------
% 12.61/5.05 % (30612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30612)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30612)Termination reason: Instruction limit
% 12.61/5.05 % (30612)Termination phase: Property scanning
% 12.61/5.05 % (30612)Time elapsed: 0.058 s
% 12.61/5.05 % (30612)Peak memory usage: 112 MB
% 12.61/5.05 % (30612)Instructions burned: 138 (million)
% 12.61/5.05 % (30613)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1285052650:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/141Mi)
% 12.61/5.05 % (30615)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=583208788:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 12.61/5.05 % (30613)Instruction limit reached!
% 12.61/5.05 % (30613)------------------------------
% 12.61/5.05 % (30613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30613)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30613)Termination reason: Instruction limit
% 12.61/5.05 % (30613)Termination phase: Saturation
% 12.61/5.05 % (30613)Time elapsed: 0.120 s
% 12.61/5.05 % (30613)Peak memory usage: 117 MB
% 12.61/5.05 % (30613)Instructions burned: 142 (million)
% 12.61/5.05 % (30618)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=1003267755:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi)
% 12.61/5.05 % (30615)Instruction limit reached!
% 12.61/5.05 % (30615)------------------------------
% 12.61/5.05 % (30615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30615)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30615)Termination reason: Instruction limit
% 12.61/5.05 % (30615)Termination phase: Saturation
% 12.61/5.05 % (30615)Time elapsed: 0.276 s
% 12.61/5.05 % (30615)Peak memory usage: 119 MB
% 12.61/5.05 % (30615)Instructions burned: 432 (million)
% 12.61/5.05 % (30620)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=2586265774:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 12.61/5.05 % (30620)Instruction limit reached!
% 12.61/5.05 % (30620)------------------------------
% 12.61/5.05 % (30620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/5.05 % (30620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/5.05 % (30620)CaDiCaL version: 2.1.3
% 12.61/5.05 % (30620)Termination reason: Instruction limit
% 12.61/5.05 % (30620)Termination phase: Preprocessing 1
% 12.61/5.05 % (30620)Time elapsed: 0.124 s
% 12.61/5.05 % (30620)Peak memory usage: 113 MB
% 12.61/5.05 % (30620)Instructions burned: 151 (million)
% 12.61/5.05 % (30622)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1136753378:i=14155:bd=all_2967 on theBenchmark for (2967ds/14155Mi)
% 12.61/5.05 % (30567)First to succeed.
% 12.61/5.05 % (30567)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-30561"
% 12.61/5.05 % (30567)Refutation found. Thanks to Tanya!
% 12.61/5.05 % SZS status Theorem for theBenchmark
% 12.61/5.05 % SZS output start Proof for theBenchmark
% See solution above
% 28.97/5.25 % (30567)------------------------------
% 28.97/5.25 % (30567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.97/5.25 % (30567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.97/5.25 % (30567)CaDiCaL version: 2.1.3
% 28.97/5.25 % (30567)Termination reason: Refutation
% 28.97/5.25 % (30567)Time elapsed: 3.603 s
% 28.97/5.25 % (30567)Peak memory usage: 230 MB
% 28.97/5.25 % (30567)Instructions burned: 8406 (million)
% 28.97/5.25 % (30567)------------------------------
% 28.97/5.25 % (30567)------------------------------
% 28.97/5.25 % (30561)Success in time 4.444 s
% 28.97/5.25 % Vampire exiting
%------------------------------------------------------------------------------