%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU430+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:53:17 PM UTC 2026
% Result : Theorem 76.45s 16.71s
% Output : Refutation 76.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 7
% Syntax : Number of formulae : 59 ( 11 unt; 0 def)
% Number of atoms : 208 ( 98 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 248 ( 99 ~; 85 |; 53 &)
% ( 5 <=>; 5 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-4 aty)
% Number of variables : 114 ( 90 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X0,X1] :
( X1 = k3_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+1.ax',d4_tarski) ).
fof(f29,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+2.ax',d1_xboole_0) ).
fof(f532,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> k5_setfam_1(X0,X1) = k3_tarski(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+8.ax',redefinition_k5_setfam_1) ).
fof(f1461,axiom,
! [X0] :
~ ( X0 != k1_xboole_0
& ! [X1] :
~ ( r2_hidden(X1,X0)
& ! [X2,X3,X4,X5] :
~ ( ( r2_hidden(X2,X0)
| r2_hidden(X3,X0) )
& X1 = k4_mcart_1(X2,X3,X4,X5) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+18.ax',t34_mcart_1) ).
fof(f2485,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+54.ax',t51_card_1) ).
fof(f2787,axiom,
! [X0] :
( ~ ( ? [X1] :
( X1 != k1_xboole_0
& r2_hidden(X1,X0) )
& k3_tarski(X0) = k1_xboole_0 )
& ~ ( k3_tarski(X0) != k1_xboole_0
& ! [X1] :
~ ( X1 != k1_xboole_0
& r2_hidden(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+59.ax',t91_orders_1) ).
fof(f4502,conjecture,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ( k5_setfam_1(X0,X1) = k1_xboole_0
<=> ! [X2] :
( r2_hidden(X2,X1)
=> X2 = k1_xboole_0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_relset_2) ).
fof(f4503,negated_conjecture,
~ ! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ( k5_setfam_1(X0,X1) = k1_xboole_0
<=> ! [X2] :
( r2_hidden(X2,X1)
=> X2 = k1_xboole_0 ) ) ),
inference(negated_conjecture,[status(cth)],[f4502]) ).
fof(f4590,plain,
! [X0] :
( ~ ( ? [X1] :
( X1 != k1_xboole_0
& r2_hidden(X1,X0) )
& k3_tarski(X0) = k1_xboole_0 )
& ~ ( k3_tarski(X0) != k1_xboole_0
& ! [X2] :
~ ( k1_xboole_0 != X2
& r2_hidden(X2,X0) ) ) ),
inference(rectify,[],[f2787]) ).
fof(f5083,plain,
! [X0,X1] :
( k5_setfam_1(X0,X1) = k3_tarski(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f532]) ).
fof(f6057,plain,
! [X0] :
( k1_xboole_0 = X0
| ? [X1] :
( r2_hidden(X1,X0)
& ! [X2,X3,X4,X5] :
( ( ~ r2_hidden(X2,X0)
& ~ r2_hidden(X3,X0) )
| k4_mcart_1(X2,X3,X4,X5) != X1 ) ) ),
inference(ennf_transformation,[],[f1461]) ).
fof(f7436,plain,
! [X0] :
( ( ! [X1] :
( k1_xboole_0 = X1
| ~ r2_hidden(X1,X0) )
| k3_tarski(X0) != k1_xboole_0 )
& ( k3_tarski(X0) = k1_xboole_0
| ? [X2] :
( k1_xboole_0 != X2
& r2_hidden(X2,X0) ) ) ),
inference(ennf_transformation,[],[f4590]) ).
fof(f9756,plain,
? [X0,X1] :
( ( k5_setfam_1(X0,X1) = k1_xboole_0
<~> ! [X2] :
( X2 = k1_xboole_0
| ~ r2_hidden(X2,X1) ) )
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f4503]) ).
fof(f10040,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ? [X2] :
( ( ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) )
& ( ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) ) )
& ( ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f10041,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ? [X2] :
( ( ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) )
& ( ? [X4] :
( r2_hidden(X2,X4)
& r2_hidden(X4,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X5] :
( ( r2_hidden(X5,X1)
| ! [X6] :
( ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ) )
& ( ? [X7] :
( r2_hidden(X5,X7)
& r2_hidden(X7,X0) )
| ~ r2_hidden(X5,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(rectify,[],[f10040]) ).
fof(f10042,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ( ( ! [X3] :
( ~ r2_hidden(sK181(X0,X1),X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(sK181(X0,X1),X1) )
& ( ( r2_hidden(sK181(X0,X1),sK182(X0,X1))
& r2_hidden(sK182(X0,X1),X0) )
| r2_hidden(sK181(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( r2_hidden(X5,X1)
| ! [X6] :
( ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ) )
& ( ( r2_hidden(X5,sK183(X0,X5))
& r2_hidden(sK183(X0,X5),X0) )
| ~ r2_hidden(X5,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK181,sK182,sK183]),skolemize(X2,sK181(X0,X1)),skolemize(X4,sK182(X0,X1)),skolemize(X7,sK183(X0,X5))],[f10041]) ).
fof(f10054,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X1] : ~ r2_hidden(X1,X0)
| k1_xboole_0 != X0 ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f10055,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(rectify,[],[f10054]) ).
fof(f10056,plain,
! [X0] :
( ( X0 = k1_xboole_0
| r2_hidden(sK197(X0),X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK197]),skolemize(X1,sK197(X0))],[f10055]) ).
fof(f10626,plain,
! [X0] :
( k1_xboole_0 = X0
| ( r2_hidden(sK524(X0),X0)
& ! [X2,X3,X4,X5] :
( ( ~ r2_hidden(X2,X0)
& ~ r2_hidden(X3,X0) )
| k4_mcart_1(X2,X3,X4,X5) != sK524(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK524]),skolemize(X1,sK524(X0))],[f6057]) ).
fof(f11369,plain,
! [X0] :
( ( ! [X1] :
( k1_xboole_0 = X1
| ~ r2_hidden(X1,X0) )
| k3_tarski(X0) != k1_xboole_0 )
& ( k3_tarski(X0) = k1_xboole_0
| ( k1_xboole_0 != sK996(X0)
& r2_hidden(sK996(X0),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK996]),skolemize(X2,sK996(X0))],[f7436]) ).
fof(f12190,plain,
? [X0,X1] :
( ( ? [X2] :
( k1_xboole_0 != X2
& r2_hidden(X2,X1) )
| k1_xboole_0 != k5_setfam_1(X0,X1) )
& ( ! [X2] :
( X2 = k1_xboole_0
| ~ r2_hidden(X2,X1) )
| k5_setfam_1(X0,X1) = k1_xboole_0 )
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(nnf_transformation,[],[f9756]) ).
fof(f12191,plain,
? [X0,X1] :
( ( ? [X2] :
( k1_xboole_0 != X2
& r2_hidden(X2,X1) )
| k1_xboole_0 != k5_setfam_1(X0,X1) )
& ( ! [X2] :
( X2 = k1_xboole_0
| ~ r2_hidden(X2,X1) )
| k5_setfam_1(X0,X1) = k1_xboole_0 )
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(flattening,[],[f12190]) ).
fof(f12192,plain,
? [X0,X1] :
( ( ? [X2] :
( k1_xboole_0 != X2
& r2_hidden(X2,X1) )
| k1_xboole_0 != k5_setfam_1(X0,X1) )
& ( ! [X3] :
( k1_xboole_0 = X3
| ~ r2_hidden(X3,X1) )
| k5_setfam_1(X0,X1) = k1_xboole_0 )
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(rectify,[],[f12191]) ).
fof(f12193,plain,
( ( ( k1_xboole_0 != sK1510
& r2_hidden(sK1510,sK1509) )
| k1_xboole_0 != k5_setfam_1(sK1508,sK1509) )
& ( ! [X3] :
( k1_xboole_0 = X3
| ~ r2_hidden(X3,sK1509) )
| k1_xboole_0 = k5_setfam_1(sK1508,sK1509) )
& m1_subset_1(sK1509,k1_zfmisc_1(k1_zfmisc_1(sK1508))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1508,sK1509,sK1510]),skolemize(X0,sK1508),skolemize(X1,sK1509),skolemize(X2,sK1510)],[f12192]) ).
fof(f12212,plain,
! [X0,X1,X6,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f10042]) ).
fof(f12243,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f10056]) ).
fof(f12941,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| k3_tarski(X1) = k5_setfam_1(X0,X1) ),
inference(cnf_transformation,[],[f5083]) ).
fof(f14300,plain,
! [X0] :
( k1_xboole_0 = X0
| r2_hidden(sK524(X0),X0) ),
inference(cnf_transformation,[],[f10626]) ).
fof(f16593,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f2485]) ).
fof(f17037,plain,
! [X0] :
( k3_tarski(X0) = k1_xboole_0
| r2_hidden(sK996(X0),X0) ),
inference(cnf_transformation,[],[f11369]) ).
fof(f17038,plain,
! [X0] :
( k3_tarski(X0) = k1_xboole_0
| k1_xboole_0 != sK996(X0) ),
inference(cnf_transformation,[],[f11369]) ).
fof(f20378,plain,
m1_subset_1(sK1509,k1_zfmisc_1(k1_zfmisc_1(sK1508))),
inference(cnf_transformation,[],[f12193]) ).
fof(f20379,plain,
! [X3] :
( k1_xboole_0 = X3
| ~ r2_hidden(X3,sK1509)
| k1_xboole_0 = k5_setfam_1(sK1508,sK1509) ),
inference(cnf_transformation,[],[f12193]) ).
fof(f20380,plain,
( r2_hidden(sK1510,sK1509)
| k1_xboole_0 != k5_setfam_1(sK1508,sK1509) ),
inference(cnf_transformation,[],[f12193]) ).
fof(f20381,plain,
( k1_xboole_0 != sK1510
| k1_xboole_0 != k5_setfam_1(sK1508,sK1509) ),
inference(cnf_transformation,[],[f12193]) ).
fof(f20406,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| np__0 != X0 ),
inference(definition_unfolding,[],[f12243,f16593]) ).
fof(f20980,plain,
! [X0] :
( r2_hidden(sK524(X0),X0)
| np__0 = X0 ),
inference(definition_unfolding,[],[f14300,f16593]) ).
fof(f21882,plain,
! [X0] :
( np__0 != sK996(X0)
| k3_tarski(X0) = np__0 ),
inference(definition_unfolding,[],[f17038,f16593,f16593]) ).
fof(f21883,plain,
! [X0] :
( r2_hidden(sK996(X0),X0)
| k3_tarski(X0) = np__0 ),
inference(definition_unfolding,[],[f17037,f16593]) ).
fof(f22340,plain,
( np__0 != k5_setfam_1(sK1508,sK1509)
| np__0 != sK1510 ),
inference(definition_unfolding,[],[f20381,f16593,f16593]) ).
fof(f22341,plain,
( np__0 != k5_setfam_1(sK1508,sK1509)
| r2_hidden(sK1510,sK1509) ),
inference(definition_unfolding,[],[f20380,f16593]) ).
fof(f22342,plain,
! [X3] :
( ~ r2_hidden(X3,sK1509)
| np__0 = X3
| np__0 = k5_setfam_1(sK1508,sK1509) ),
inference(definition_unfolding,[],[f20379,f16593,f16593]) ).
fof(f22351,plain,
! [X0,X6,X5] :
( ~ r2_hidden(X6,X0)
| ~ r2_hidden(X5,X6)
| r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f12212]) ).
fof(f22356,plain,
! [X2] : ~ r2_hidden(X2,np__0),
inference(equality_resolution,[],[f20406]) ).
fof(f49146,plain,
( np__0 = k3_tarski(sK1509)
| np__0 = sK996(sK1509)
| np__0 = k5_setfam_1(sK1508,sK1509) ),
inference(resolution,[],[f21883,f22342]) ).
fof(f49156,plain,
( np__0 = k5_setfam_1(sK1508,sK1509)
| np__0 = k3_tarski(sK1509) ),
inference(forward_subsumption_resolution,[],[f49146,f21882]) ).
fof(f102877,plain,
k5_setfam_1(sK1508,sK1509) = k3_tarski(sK1509),
inference(resolution,[],[f12941,f20378]) ).
fof(f102920,plain,
( np__0 != k3_tarski(sK1509)
| np__0 != sK1510 ),
inference(superposition,[],[f22340,f102877]) ).
fof(f102921,plain,
( np__0 != k3_tarski(sK1509)
| r2_hidden(sK1510,sK1509) ),
inference(superposition,[],[f22341,f102877]) ).
fof(f102950,plain,
( np__0 = k3_tarski(sK1509)
| np__0 = k3_tarski(sK1509) ),
inference(superposition,[],[f49156,f102877]) ).
fof(f102952,plain,
np__0 = k3_tarski(sK1509),
inference(duplicate_literal_removal,[],[f102950]) ).
fof(f102955,plain,
r2_hidden(sK1510,sK1509),
inference(forward_subsumption_resolution,[],[f102921,f102952]) ).
fof(f102956,plain,
np__0 != sK1510,
inference(forward_subsumption_resolution,[],[f102920,f102952]) ).
fof(f102996,plain,
! [X0] :
( ~ r2_hidden(X0,sK1510)
| r2_hidden(X0,k3_tarski(sK1509)) ),
inference(resolution,[],[f102955,f22351]) ).
fof(f103001,plain,
! [X0] :
( r2_hidden(X0,np__0)
| ~ r2_hidden(X0,sK1510) ),
inference(forward_demodulation,[],[f102996,f102952]) ).
fof(f103009,plain,
! [X0] : ~ r2_hidden(X0,sK1510),
inference(forward_subsumption_resolution,[],[f103001,f22356]) ).
fof(f103369,plain,
np__0 = sK1510,
inference(resolution,[],[f103009,f20980]) ).
fof(f103388,plain,
$false,
inference(forward_subsumption_resolution,[],[f103369,f102956]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU430+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 05:25:27 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.12/2.64 % (1243839)Will run a generic schedule for satisfiability detection.
% 14.12/2.64 % (1243849)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3657312564:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 14.12/2.64 % (1243845)% WARNING: option uhcvi not known.
% 14.12/2.64 % (1243844)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2512401719_2998 on theBenchmark for (2998ds/0Mi)
% 14.12/2.64 % (1243846)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4061662921:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 14.12/2.64 % (1243845)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2802015765:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 14.12/2.64 % (1243847)dis+10_1_sil=32000:sp=arity:random_seed=2609802565:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 14.12/2.64 % (1243848)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2747180884:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 14.12/2.64 % (1243850)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1841405890:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 14.12/2.64 % (1243849)Instruction limit reached!
% 14.12/2.64 % (1243849)------------------------------
% 14.12/2.64 % (1243849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.12/2.64 % (1243849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.12/2.64 % (1243849)CaDiCaL version: 2.1.3
% 14.12/2.64 % (1243849)Termination reason: Instruction limit
% 14.12/2.64 % (1243849)Termination phase: Preprocessing 3
% 14.12/2.64 % (1243849)Time elapsed: 0.050 s
% 14.12/2.64 % (1243849)Peak memory usage: 22 MB
% 14.12/2.64 % (1243849)Instructions burned: 133 (million)
% 14.12/2.64 % (1243858)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3335006083:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 14.12/2.64 % (1243847)Instruction limit reached!
% 14.12/2.64 % (1243847)------------------------------
% 14.12/2.64 % (1243847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.12/2.64 % (1243847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.12/2.64 % (1243847)CaDiCaL version: 2.1.3
% 14.12/2.64 % (1243847)Termination reason: Instruction limit
% 14.12/2.64 % (1243847)Termination phase: Preprocessing 3
% 14.12/2.64 % (1243847)Time elapsed: 0.070 s
% 14.12/2.64 % (1243847)Peak memory usage: 21 MB
% 14.12/2.64 % (1243847)Instructions burned: 103 (million)
% 14.12/2.64 % (1243848)Instruction limit reached!
% 14.12/2.64 % (1243848)------------------------------
% 14.12/2.64 % (1243848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.12/2.64 % (1243848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.12/2.64 % (1243848)CaDiCaL version: 2.1.3
% 14.12/2.64 % (1243848)Termination reason: Instruction limit
% 14.12/2.64 % (1243848)Termination phase: NewCNF
% 14.12/2.64 % (1243848)Time elapsed: 0.078 s
% 14.12/2.64 % (1243848)Peak memory usage: 23 MB
% 14.12/2.64 % (1243848)Instructions burned: 117 (million)
% 14.12/2.64 % (1243860)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=595647401:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 14.12/2.64 % (1243861)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=972349268:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 14.12/2.64 % (1243850)Instruction limit reached!
% 14.12/2.64 % (1243850)------------------------------
% 14.12/2.64 % (1243850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.12/2.64 % (1243850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.12/2.64 % (1243850)CaDiCaL version: 2.1.3
% 14.12/2.64 % (1243850)Termination reason: Instruction limit
% 14.12/2.64 % (1243850)Termination phase: Clausification
% 14.12/2.64 % (1243850)Time elapsed: 0.102 s
% 14.12/2.64 % (1243850)Peak memory usage: 24 MB
% 14.12/2.64 % (1243850)Instructions burned: 159 (million)
% 14.12/2.64 % (1243864)ott-21_1_sil=16000:fs=off:random_seed=1638423775:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 14.12/2.64 % (1243860)Instruction limit reached!
% 14.12/2.64 % (1243860)------------------------------
% 14.12/2.64 % (1243860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.12/2.64 % (1243860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.55/4.91 % (1243860)CaDiCaL version: 2.1.3
% 30.55/4.91 % (1243860)Termination reason: Instruction limit
% 30.55/4.91 % (1243860)Termination phase: Preprocessing 3
% 30.55/4.91 % (1243860)Time elapsed: 0.087 s
% 30.55/4.91 % (1243860)Peak memory usage: 22 MB
% 30.55/4.91 % (1243860)Instructions burned: 133 (million)
% 30.55/4.91 % (1243866)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2207474202:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 30.55/4.91 % (1243864)Instruction limit reached!
% 30.55/4.91 % (1243864)------------------------------
% 30.55/4.91 % (1243864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.55/4.91 % (1243864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.55/4.91 % (1243864)CaDiCaL version: 2.1.3
% 30.55/4.91 % (1243864)Termination reason: Instruction limit
% 30.55/4.91 % (1243864)Termination phase: Property scanning
% 30.55/4.91 % (1243864)Time elapsed: 0.114 s
% 30.55/4.91 % (1243864)Peak memory usage: 25 MB
% 30.55/4.91 % (1243864)Instructions burned: 181 (million)
% 30.55/4.91 % (1243868)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2707865221:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 30.55/4.91 % (1243858)Instruction limit reached!
% 30.55/4.91 % (1243858)------------------------------
% 30.55/4.91 % (1243858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.55/4.91 % (1243858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.55/4.91 % (1243858)CaDiCaL version: 2.1.3
% 30.55/4.91 % (1243858)Termination reason: Instruction limit
% 30.55/4.91 % (1243858)Termination phase: Finite model building preprocessing
% 30.55/4.91 % (1243858)Time elapsed: 0.207 s
% 30.55/4.91 % (1243858)Peak memory usage: 35 MB
% 30.55/4.91 % (1243858)Instructions burned: 715 (million)
% 30.55/4.91 % (1243870)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2474068830:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 30.55/4.91 % (1243866)Instruction limit reached!
% 30.55/4.91 % (1243866)------------------------------
% 30.55/4.91 % (1243866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.55/4.91 % (1243866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.55/4.91 % (1243866)CaDiCaL version: 2.1.3
% 30.55/4.91 % (1243866)Termination reason: Instruction limit
% 30.55/4.91 % (1243866)Termination phase: Saturation
% 30.55/4.91 % (1243866)Time elapsed: 0.256 s
% 30.55/4.91 % (1243866)Peak memory usage: 29 MB
% 30.55/4.91 % (1243866)Instructions burned: 477 (million)
% 30.55/4.91 % (1243861)Instruction limit reached!
% 30.55/4.91 % (1243861)------------------------------
% 30.55/4.91 % (1243861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.55/4.91 % (1243861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.55/4.91 % (1243861)CaDiCaL version: 2.1.3
% 30.55/4.91 % (1243861)Termination reason: Instruction limit
% 30.55/4.91 % (1243861)Termination phase: Saturation
% 30.55/4.91 % (1243861)Time elapsed: 0.361 s
% 30.55/4.91 % (1243861)Peak memory usage: 31 MB
% 30.55/4.91 % (1243861)Instructions burned: 684 (million)
% 30.55/4.91 % (1243872)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2382090924:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 30.55/4.91 % (1243873)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1594237269:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 30.55/4.91 % (1243870)Instruction limit reached!
% 30.55/4.91 % (1243870)------------------------------
% 30.55/4.91 % (1243870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.55/4.91 % (1243870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.55/4.91 % (1243870)CaDiCaL version: 2.1.3
% 30.55/4.91 % (1243870)Termination reason: Instruction limit
% 30.55/4.91 % (1243870)Termination phase: Saturation
% 30.55/4.91 % (1243870)Time elapsed: 0.360 s
% 30.55/4.91 % (1243870)Peak memory usage: 42 MB
% 30.55/4.91 % (1243870)Instructions burned: 1179 (million)
% 30.55/4.91 % (1243876)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=28341833:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 30.55/4.91 % (1243868)Instruction limit reached!
% 30.55/4.91 % (1243868)------------------------------
% 30.55/4.91 % (1243868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.55/4.91 % (1243868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.23/9.69 % (1243868)CaDiCaL version: 2.1.3
% 64.23/9.69 % (1243868)Termination reason: Instruction limit
% 64.23/9.69 % (1243868)Termination phase: Finite model building preprocessing
% 64.23/9.69 % (1243868)Time elapsed: 0.442 s
% 64.23/9.69 % (1243868)Peak memory usage: 34 MB
% 64.23/9.69 % (1243868)Instructions burned: 866 (million)
% 64.23/9.69 % (1243878)fmb+10_1_sil=64000:random_seed=2019627606:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 64.23/9.69 % (1243873)Instruction limit reached!
% 64.23/9.69 % (1243873)------------------------------
% 64.23/9.69 % (1243873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.23/9.69 % (1243873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.23/9.69 % (1243873)CaDiCaL version: 2.1.3
% 64.23/9.69 % (1243873)Termination reason: Instruction limit
% 64.23/9.69 % (1243873)Termination phase: Saturation
% 64.23/9.69 % (1243873)Time elapsed: 0.379 s
% 64.23/9.69 % (1243873)Peak memory usage: 34 MB
% 64.23/9.69 % (1243873)Instructions burned: 693 (million)
% 64.23/9.69 % (1243880)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=536469945:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 64.23/9.69 % (1243876)Instruction limit reached!
% 64.23/9.69 % (1243876)------------------------------
% 64.23/9.69 % (1243876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.23/9.69 % (1243876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.23/9.69 % (1243876)CaDiCaL version: 2.1.3
% 64.23/9.69 % (1243876)Termination reason: Instruction limit
% 64.23/9.69 % (1243876)Termination phase: Saturation
% 64.23/9.69 % (1243876)Time elapsed: 0.236 s
% 64.23/9.69 % (1243876)Peak memory usage: 39 MB
% 64.23/9.69 % (1243876)Instructions burned: 884 (million)
% 64.23/9.69 % (1243882)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3956290214:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 64.23/9.69 % (1243872)Instruction limit reached!
% 64.23/9.69 % (1243872)------------------------------
% 64.23/9.69 % (1243872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.23/9.69 % (1243872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.23/9.69 % (1243872)CaDiCaL version: 2.1.3
% 64.23/9.69 % (1243872)Termination reason: Instruction limit
% 64.23/9.69 % (1243872)Termination phase: Finite model building preprocessing
% 64.23/9.69 % (1243872)Time elapsed: 0.455 s
% 64.23/9.69 % (1243872)Peak memory usage: 35 MB
% 64.23/9.69 % (1243872)Instructions burned: 890 (million)
% 64.23/9.69 % (1243884)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=243698180:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 64.23/9.69 % (1243882)Instruction limit reached!
% 64.23/9.69 % (1243882)------------------------------
% 64.23/9.69 % (1243882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.23/9.69 % (1243882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.23/9.69 % (1243882)CaDiCaL version: 2.1.3
% 64.23/9.69 % (1243882)Termination reason: Instruction limit
% 64.23/9.69 % (1243882)Termination phase: Finite model building preprocessing
% 64.23/9.69 % (1243882)Time elapsed: 0.252 s
% 64.23/9.69 % (1243882)Peak memory usage: 34 MB
% 64.23/9.69 % (1243882)Instructions burned: 922 (million)
% 64.23/9.69 % (1243886)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3712846400:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 64.23/9.69 % Detected minimum model sizes of [5]
% 64.23/9.69 % Detected maximum model sizes of [max]
% 64.23/9.69 % TRYING [5]
% 64.23/9.69 % (1243886)Instruction limit reached!
% 64.23/9.69 % (1243886)------------------------------
% 64.23/9.69 % (1243886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.23/9.69 % (1243886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.23/9.69 % (1243886)CaDiCaL version: 2.1.3
% 64.23/9.69 % (1243886)Termination reason: Instruction limit
% 64.23/9.69 % (1243886)Termination phase: Saturation
% 64.23/9.69 % (1243886)Time elapsed: 0.387 s
% 64.23/9.69 % (1243886)Peak memory usage: 35 MB
% 64.23/9.69 % (1243886)Instructions burned: 1478 (million)
% 64.23/9.69 % (1243888)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=953727304:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 64.23/9.69 % Detected minimum model sizes of [5]
% 64.23/9.69 % Detected maximum model sizes of [max]
% 64.23/9.69 % Detected minimum model sizes of [5]
% 64.23/9.69 % Detected maximum model sizes of [max]
% 64.23/9.69 % (1243880)Cannot represent all propositional literals internally
% 64.23/9.69 % (1243880)Refutation not found, incomplete strategy
% 108.91/15.97 % (1243880)------------------------------
% 108.91/15.97 % (1243880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.91/15.97 % (1243880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.91/15.97 % (1243880)CaDiCaL version: 2.1.3
% 108.91/15.97 % (1243880)Termination reason: Refutation not found, incomplete strategy
% 108.91/15.97 % (1243880)Time elapsed: 1.160 s
% 108.91/15.97 % (1243880)Peak memory usage: 58 MB
% 108.91/15.97 % (1243880)Instructions burned: 2333 (million)
% 108.91/15.97 % (1243880)------------------------------
% 108.91/15.97 % (1243880)------------------------------
% 108.91/15.97 % (1243890)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1248124743:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 108.91/15.97 % Detected minimum model sizes of [5]
% 108.91/15.97 % Detected maximum model sizes of [max]
% 108.91/15.97 % (1243888)Cannot represent all propositional literals internally
% 108.91/15.97 % (1243888)Refutation not found, incomplete strategy
% 108.91/15.97 % (1243888)------------------------------
% 108.91/15.97 % (1243888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.91/15.97 % (1243888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.91/15.97 % (1243888)CaDiCaL version: 2.1.3
% 108.91/15.97 % (1243888)Termination reason: Refutation not found, incomplete strategy
% 108.91/15.97 % (1243888)Time elapsed: 0.764 s
% 108.91/15.97 % (1243888)Peak memory usage: 62 MB
% 108.91/15.97 % (1243888)Instructions burned: 2784 (million)
% 108.91/15.97 % (1243888)------------------------------
% 108.91/15.97 % (1243888)------------------------------
% 108.91/15.97 % (1243892)ott-2_1_sil=16000:newcnf=on:random_seed=2002458839:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2974 on theBenchmark for (2974ds/869Mi)
% 108.91/15.97 % (1243892)Instruction limit reached!
% 108.91/15.97 % (1243892)------------------------------
% 108.91/15.97 % (1243892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.91/15.97 % (1243892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.91/15.97 % (1243892)CaDiCaL version: 2.1.3
% 108.91/15.97 % (1243892)Termination reason: Instruction limit
% 108.91/15.97 % (1243892)Termination phase: Saturation
% 108.91/15.97 % (1243892)Time elapsed: 0.242 s
% 108.91/15.97 % (1243892)Peak memory usage: 34 MB
% 108.91/15.97 % (1243892)Instructions burned: 870 (million)
% 108.91/15.97 % (1243894)ott+10_1_sil=32000:tgt=ground:random_seed=111424896:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi)
% 108.91/15.97 % (1243890)Instruction limit reached!
% 108.91/15.97 % (1243890)------------------------------
% 108.91/15.97 % (1243890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.91/15.97 % (1243890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.91/15.97 % (1243890)CaDiCaL version: 2.1.3
% 108.91/15.97 % (1243890)Termination reason: Instruction limit
% 108.91/15.97 % (1243890)Termination phase: Finite model building preprocessing
% 108.91/15.97 % (1243890)Time elapsed: 1.052 s
% 108.91/15.97 % (1243890)Peak memory usage: 48 MB
% 108.91/15.97 % (1243890)Instructions burned: 2176 (million)
% 108.91/15.97 % (1243896)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2191633901:i=54282_2966 on theBenchmark for (2966ds/54282Mi)
% 108.91/15.97 % (1243884)Instruction limit reached!
% 108.91/15.97 % (1243884)------------------------------
% 108.91/15.97 % (1243884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.91/15.97 % (1243884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.91/15.97 % (1243884)CaDiCaL version: 2.1.3
% 108.91/15.97 % (1243884)Termination reason: Instruction limit
% 108.91/15.97 % (1243884)Termination phase: Saturation
% 108.91/15.97 % (1243884)Time elapsed: 2.985 s
% 108.91/15.97 % (1243884)Peak memory usage: 77 MB
% 108.91/15.97 % (1243884)Instructions burned: 5131 (million)
% 108.91/15.97 % (1243898)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2971858708:i=3512:aac=none_2958 on theBenchmark for (2958ds/3512Mi)
% 108.91/15.97 % (1243894)Instruction limit reached!
% 108.91/15.97 % (1243894)------------------------------
% 108.91/15.97 % (1243894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.91/15.97 % (1243894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.91/15.97 % (1243894)CaDiCaL version: 2.1.3
% 108.91/15.97 % (1243894)Termination reason: Instruction limit
% 108.91/15.97 % (1243894)Termination phase: Saturation
% 108.91/15.97 % (1243894)Time elapsed: 1.701 s
% 108.91/15.97 % (1243894)Peak memory usage: 89 MB
% 108.91/15.97 % (1243894)Instructions burned: 5115 (million)
% 76.45/16.71 % (1243900)dis+21_1_sil=32000:sas=cadical:random_seed=1047583521:i=3773:amm=off_2954 on theBenchmark for (2954ds/3773Mi)
% 76.45/16.71 % Detected minimum model sizes of [5]
% 76.45/16.71 % Detected maximum model sizes of [max]
% 76.45/16.71 % TRYING [5]
% 76.45/16.71 % (1243900)Instruction limit reached!
% 76.45/16.71 % (1243900)------------------------------
% 76.45/16.71 % (1243900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243900)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243900)Termination reason: Instruction limit
% 76.45/16.71 % (1243900)Termination phase: Saturation
% 76.45/16.71 % (1243900)Time elapsed: 1.083 s
% 76.45/16.71 % (1243900)Peak memory usage: 56 MB
% 76.45/16.71 % (1243900)Instructions burned: 3774 (million)
% 76.45/16.71 % (1243902)ott+11_1_sil=16000:gs=on:random_seed=3094610536:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2943 on theBenchmark for (2943ds/2251Mi)
% 76.45/16.71 % (1243898)Instruction limit reached!
% 76.45/16.71 % (1243898)------------------------------
% 76.45/16.71 % (1243898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243898)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243898)Termination reason: Instruction limit
% 76.45/16.71 % (1243898)Termination phase: Saturation
% 76.45/16.71 % (1243898)Time elapsed: 1.947 s
% 76.45/16.71 % (1243898)Peak memory usage: 59 MB
% 76.45/16.71 % (1243898)Instructions burned: 3513 (million)
% 76.45/16.71 % (1243904)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3677119177:fmbsr=1.6:i=67534_2938 on theBenchmark for (2938ds/67534Mi)
% 76.45/16.71 % (1243902)Instruction limit reached!
% 76.45/16.71 % (1243902)------------------------------
% 76.45/16.71 % (1243902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243902)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243902)Termination reason: Instruction limit
% 76.45/16.71 % (1243902)Termination phase: Saturation
% 76.45/16.71 % (1243902)Time elapsed: 0.586 s
% 76.45/16.71 % (1243902)Peak memory usage: 43 MB
% 76.45/16.71 % (1243902)Instructions burned: 2254 (million)
% 76.45/16.71 % (1243906)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3058583760:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2937 on theBenchmark for (2937ds/4591Mi)
% 76.45/16.71 % (1243906)Instruction limit reached!
% 76.45/16.71 % (1243906)------------------------------
% 76.45/16.71 % (1243906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243906)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243906)Termination reason: Instruction limit
% 76.45/16.71 % (1243906)Termination phase: Saturation
% 76.45/16.71 % (1243906)Time elapsed: 0.993 s
% 76.45/16.71 % (1243906)Peak memory usage: 40 MB
% 76.45/16.71 % (1243906)Instructions burned: 4592 (million)
% 76.45/16.71 % (1243908)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=206258223:i=29340_2927 on theBenchmark for (2927ds/29340Mi)
% 76.45/16.71 % Detected minimum model sizes of [5]
% 76.45/16.71 % Detected maximum model sizes of [max]
% 76.45/16.71 % (1243904)Cannot represent all propositional literals internally
% 76.45/16.71 % (1243904)Refutation not found, incomplete strategy
% 76.45/16.71 % (1243904)------------------------------
% 76.45/16.71 % (1243904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243904)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243904)Termination reason: Refutation not found, incomplete strategy
% 76.45/16.71 % (1243904)Time elapsed: 1.293 s
% 76.45/16.71 % (1243904)Peak memory usage: 57 MB
% 76.45/16.71 % (1243904)Instructions burned: 2748 (million)
% 76.45/16.71 % (1243904)------------------------------
% 76.45/16.71 % (1243904)------------------------------
% 76.45/16.71 % (1243910)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=594812029:i=5211_2925 on theBenchmark for (2925ds/5211Mi)
% 76.45/16.71 % (1243910)Instruction limit reached!
% 76.45/16.71 % (1243910)------------------------------
% 76.45/16.71 % (1243910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243910)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243910)Termination reason: Instruction limit
% 76.45/16.71 % (1243910)Termination phase: Saturation
% 76.45/16.71 % (1243910)Time elapsed: 1.819 s
% 76.45/16.71 % (1243910)Peak memory usage: 49 MB
% 76.45/16.71 % (1243910)Instructions burned: 5212 (million)
% 76.45/16.71 % (1243912)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2846414400:i=5497:nm=2_2907 on theBenchmark for (2907ds/5497Mi)
% 76.45/16.71 % (1243878)Instruction limit reached!
% 76.45/16.71 % (1243878)------------------------------
% 76.45/16.71 % (1243878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243878)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243878)Termination reason: Instruction limit
% 76.45/16.71 % (1243878)Termination phase: Finite model building constraint generation
% 76.45/16.71 % (1243878)Time elapsed: 9.460 s
% 76.45/16.71 % (1243878)Peak memory usage: 1985 MB
% 76.45/16.71 % (1243878)Instructions burned: 22061 (million)
% 76.45/16.71 % Detected minimum model sizes of [5]
% 76.45/16.71 % Detected maximum model sizes of [max]
% 76.45/16.71 % (1243912)Cannot represent all propositional literals internally
% 76.45/16.71 % (1243912)Refutation not found, incomplete strategy
% 76.45/16.71 % (1243912)------------------------------
% 76.45/16.71 % (1243912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243912)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243912)Termination reason: Refutation not found, incomplete strategy
% 76.45/16.71 % (1243912)Time elapsed: 1.105 s
% 76.45/16.71 % (1243912)Peak memory usage: 58 MB
% 76.45/16.71 % (1243912)Instructions burned: 2146 (million)
% 76.45/16.71 % (1243912)------------------------------
% 76.45/16.71 % (1243912)------------------------------
% 76.45/16.71 % (1243914)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3312345159:fmbsr=2:i=46332_2895 on theBenchmark for (2895ds/46332Mi)
% 76.45/16.71 % (1243916)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=856116372:i=14071_2893 on theBenchmark for (2893ds/14071Mi)
% 76.45/16.71 % Detected minimum model sizes of [5]
% 76.45/16.71 % Detected maximum model sizes of [max]
% 76.45/16.71 % (1243914)Cannot represent all propositional literals internally
% 76.45/16.71 % (1243914)Refutation not found, incomplete strategy
% 76.45/16.71 % (1243914)------------------------------
% 76.45/16.71 % (1243914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243914)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243914)Termination reason: Refutation not found, incomplete strategy
% 76.45/16.71 % (1243914)Time elapsed: 1.313 s
% 76.45/16.71 % (1243914)Peak memory usage: 57 MB
% 76.45/16.71 % (1243914)Instructions burned: 2749 (million)
% 76.45/16.71 % (1243914)------------------------------
% 76.45/16.71 % (1243914)------------------------------
% 76.45/16.71 % (1243918)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=774529158:i=22565:add=on:rawr=on_2882 on theBenchmark for (2882ds/22565Mi)
% 76.45/16.71 % Detected minimum model sizes of [5]
% 76.45/16.71 % Detected maximum model sizes of [max]
% 76.45/16.71 % (1243916)Cannot represent all propositional literals internally
% 76.45/16.71 % (1243916)Refutation not found, incomplete strategy
% 76.45/16.71 % (1243916)------------------------------
% 76.45/16.71 % (1243916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243916)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243916)Termination reason: Refutation not found, incomplete strategy
% 76.45/16.71 % (1243916)Time elapsed: 1.266 s
% 76.45/16.71 % (1243916)Peak memory usage: 60 MB
% 76.45/16.71 % (1243916)Instructions burned: 2576 (million)
% 76.45/16.71 % (1243916)------------------------------
% 76.45/16.71 % (1243916)------------------------------
% 76.45/16.71 % (1243920)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3757521788:i=8173:av=off_2880 on theBenchmark for (2880ds/8173Mi)
% 76.45/16.71 % (1243908)Instruction limit reached!
% 76.45/16.71 % (1243908)------------------------------
% 76.45/16.71 % (1243908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.71 % (1243908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.71 % (1243908)CaDiCaL version: 2.1.3
% 76.45/16.71 % (1243908)Termination reason: Instruction limit
% 76.45/16.71 % (1243908)Termination phase: Saturation
% 76.45/16.71 % (1243908)Time elapsed: 8.341 s
% 76.45/16.71 % (1243908)Peak memory usage: 708 MB
% 76.45/16.71 % (1243908)Instructions burned: 29342 (million)
% 76.45/16.71 % (1243922)dis+10_16:1_sil=16000:random_seed=3204921205:i=9155:fsr=off_2843 on theBenchmark for (2843ds/9155Mi)
% 76.45/16.71 % (1243920) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1243839-1243920"...
% 76.45/16.71 % (1243920)...printing done.
% 76.45/16.71 % (1243920)Refutation found. Thanks to Tanya!
% 76.45/16.71 % SZS status Theorem for theBenchmark
% 76.45/16.71 % SZS output start Proof for theBenchmark
% See solution above
% 76.45/16.72 % (1243920)------------------------------
% 76.45/16.72 % (1243920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.45/16.72 % (1243920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.45/16.72 % (1243920)CaDiCaL version: 2.1.3
% 76.45/16.72 % (1243920)Termination reason: Refutation
% 76.45/16.72 % (1243920)Time elapsed: 3.923 s
% 76.45/16.72 % (1243920)Peak memory usage: 109 MB
% 76.45/16.72 % (1243920)Instructions burned: 7047 (million)
% 76.45/16.72 % (1243839)Success in time 16.3 s
% 76.45/16.72 % Vampire exiting
%------------------------------------------------------------------------------