%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL888+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:00:56 PM UTC 2026
% Result : Theorem 102.47s 15.02s
% Output : Refutation 102.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 14
% Syntax : Number of formulae : 101 ( 48 unt; 3 def)
% Number of atoms : 165 ( 42 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 119 ( 55 ~; 48 |; 7 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 4 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 129 ( 0 sgn 123 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] : '+'('+'(X0,X1),X2) = '+'(X0,'+'(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
fof(f2,axiom,
! [X0,X1] : '+'(X0,X1) = '+'(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f3,axiom,
! [X0] : '+'(X0,'0') = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_03) ).
fof(f4,axiom,
! [X0] : '>='(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_04) ).
fof(f6,axiom,
! [X0,X1] :
( ( '>='(X0,X1)
& '>='(X1,X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_06) ).
fof(f7,axiom,
! [X0,X1,X2] :
( '>='('+'(X0,X1),X2)
<=> '>='(X1,'==>'(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(f8,axiom,
! [X0] : '>='(X0,'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
fof(f10,axiom,
! [X0,X1,X2] :
( '>='(X0,X1)
=> '>='('==>'(X1,X2),'==>'(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_10) ).
fof(f11,axiom,
! [X0,X1,X2] :
( '>='(X0,X1)
=> '>='('==>'(X2,X0),'==>'(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_11) ).
fof(f12,axiom,
! [X0,X1] : '+'(X0,'==>'(X0,X1)) = '+'(X1,'==>'(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_12) ).
fof(f13,conjecture,
! [X0,X1,X2] :
( ( X0 = '==>'(X0,X1)
& X2 = '==>'(X2,X1) )
=> X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_13) ).
fof(f14,negated_conjecture,
~ ! [X0,X1,X2] :
( ( X0 = '==>'(X0,X1)
& X2 = '==>'(X2,X1) )
=> X0 = X2 ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f17,plain,
! [X0,X1] :
( X0 = X1
| ~ '>='(X0,X1)
| ~ '>='(X1,X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f18,plain,
! [X0,X1] :
( X0 = X1
| ~ '>='(X0,X1)
| ~ '>='(X1,X0) ),
inference(flattening,[],[f17]) ).
fof(f20,plain,
! [X0,X1,X2] :
( '>='('==>'(X1,X2),'==>'(X0,X2))
| ~ '>='(X0,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f21,plain,
! [X0,X1,X2] :
( '>='('==>'(X2,X0),'==>'(X2,X1))
| ~ '>='(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f22,plain,
? [X0,X1,X2] :
( X0 != X2
& X0 = '==>'(X0,X1)
& X2 = '==>'(X2,X1) ),
inference(ennf_transformation,[],[f14]) ).
fof(f23,plain,
? [X0,X1,X2] :
( X0 != X2
& X0 = '==>'(X0,X1)
& X2 = '==>'(X2,X1) ),
inference(flattening,[],[f22]) ).
fof(f24,plain,
! [X2,X0,X1] : '+'('+'(X0,X1),X2) = '+'(X0,'+'(X1,X2)),
inference(cnf_transformation,[],[f1]) ).
fof(f25,plain,
! [X0,X1] : '+'(X0,X1) = '+'(X1,X0),
inference(cnf_transformation,[],[f2]) ).
fof(f26,plain,
! [X0] : '+'(X0,'0') = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f27,plain,
! [X0] : '>='(X0,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f29,plain,
! [X0,X1] :
( ~ '>='(X1,X0)
| ~ '>='(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f18]) ).
fof(f30,plain,
! [X2,X0,X1] :
( ~ '>='(X1,'==>'(X0,X2))
| '>='('+'(X0,X1),X2) ),
inference(cnf_transformation,[],[f7]) ).
fof(f31,plain,
! [X2,X0,X1] :
( ~ '>='('+'(X0,X1),X2)
| '>='(X1,'==>'(X0,X2)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f32,plain,
! [X0] : '>='(X0,'0'),
inference(cnf_transformation,[],[f8]) ).
fof(f34,plain,
! [X2,X0,X1] :
( ~ '>='(X0,X1)
| '>='('==>'(X1,X2),'==>'(X0,X2)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f35,plain,
! [X2,X0,X1] :
( ~ '>='(X0,X1)
| '>='('==>'(X2,X0),'==>'(X2,X1)) ),
inference(cnf_transformation,[],[f21]) ).
fof(f36,plain,
! [X0,X1] : '+'(X0,'==>'(X0,X1)) = '+'(X1,'==>'(X1,X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f37,plain,
sK2 = '==>'(sK2,sK1),
inference(cnf_transformation,[],[f23]) ).
fof(f38,plain,
sK0 = '==>'(sK0,sK1),
inference(cnf_transformation,[],[f23]) ).
fof(f39,plain,
sK0 != sK2,
inference(cnf_transformation,[],[f23]) ).
fof(f40,plain,
! [X0] : '+'('0',X0) = X0,
inference(superposition,[],[f25,f26]) ).
fof(f47,plain,
! [X0] :
( ~ '>='('0',X0)
| '0' = X0 ),
inference(resolution,[],[f29,f32]) ).
fof(f52,plain,
! [X0,X1] : '>='('+'(X0,'==>'(X0,X1)),X1),
inference(resolution,[],[f30,f27]) ).
fof(f53,plain,
! [X0] :
( ~ '>='(X0,sK2)
| '>='('+'(sK2,X0),sK1) ),
inference(superposition,[],[f30,f37]) ).
fof(f54,plain,
! [X0] :
( ~ '>='(X0,sK0)
| '>='('+'(sK0,X0),sK1) ),
inference(superposition,[],[f30,f38]) ).
fof(f56,plain,
! [X0,X1] : '>='(X0,'==>'(X1,'0')),
inference(resolution,[],[f31,f32]) ).
fof(f57,plain,
! [X0,X1] :
( '>='('0','==>'(X0,X1))
| ~ '>='(X0,X1) ),
inference(superposition,[],[f31,f26]) ).
fof(f58,plain,
! [X2,X0,X1] :
( ~ '>='('+'(X0,X1),X2)
| '>='(X0,'==>'(X1,X2)) ),
inference(superposition,[],[f31,f25]) ).
fof(f76,plain,
! [X0,X1] : '>='('==>'('0',X0),'==>'(X1,X0)),
inference(resolution,[],[f34,f32]) ).
fof(f119,plain,
! [X2,X0,X1] : '+'(X0,'+'(X1,X2)) = '+'(X1,'+'(X2,X0)),
inference(superposition,[],[f24,f25]) ).
fof(f129,plain,
! [X0] : '==>'('0',X0) = '+'(X0,'==>'(X0,'0')),
inference(superposition,[],[f36,f40]) ).
fof(f133,plain,
! [X2,X0,X1] : '+'(X1,'+'('==>'(X1,X0),X2)) = '+'('+'(X0,'==>'(X0,X1)),X2),
inference(superposition,[],[f24,f36]) ).
fof(f153,plain,
! [X0] : '0' = '==>'(X0,'0'),
inference(resolution,[],[f47,f56]) ).
fof(f163,plain,
! [X0] : '>='('+'(sK0,'+'(X0,'==>'(X0,sK0))),sK1),
inference(resolution,[],[f52,f54]) ).
fof(f164,plain,
! [X0] : '>='('+'(sK2,'+'(X0,'==>'(X0,sK2))),sK1),
inference(resolution,[],[f52,f53]) ).
fof(f187,plain,
! [X2,X0,X1] : '>='('==>'(X0,'==>'('0',X1)),'==>'(X0,'==>'(X2,X1))),
inference(resolution,[],[f76,f35]) ).
fof(f193,plain,
! [X0,X1] :
( ~ '>='(X0,X1)
| '0' = '==>'(X0,X1) ),
inference(resolution,[],[f57,f47]) ).
fof(f449,plain,
! [X2,X3,X0,X1] :
( ~ '>='('+'(X0,'+'(X1,X2)),X3)
| '>='('+'(X2,X0),'==>'(X1,X3)) ),
inference(superposition,[],[f31,f119]) ).
fof(f779,plain,
! [X2,X3,X0,X1] :
( ~ '>='('+'('+'(X0,'==>'(X0,X1)),X2),X3)
| '>='('+'('==>'(X1,X0),X2),'==>'(X1,X3)) ),
inference(superposition,[],[f31,f133]) ).
fof(f783,plain,
! [X2,X3,X0,X1] :
( ~ '>='('+'('+'(X0,'==>'(X0,X1)),X2),X3)
| '>='(X1,'==>'('+'('==>'(X1,X0),X2),X3)) ),
inference(superposition,[],[f58,f133]) ).
fof(f832,plain,
! [X2,X3,X0,X1] :
( ~ '>='('+'(X0,'+'('==>'(X0,X1),X2)),X3)
| '>='(X1,'==>'('+'('==>'(X1,X0),X2),X3)) ),
inference(forward_demodulation,[],[f783,f24]) ).
fof(f836,plain,
! [X2,X3,X0,X1] :
( ~ '>='('+'(X0,'+'('==>'(X0,X1),X2)),X3)
| '>='('+'('==>'(X1,X0),X2),'==>'(X1,X3)) ),
inference(forward_demodulation,[],[f779,f24]) ).
fof(f2125,plain,
! [X0] : '+'(X0,'0') = '==>'('0',X0),
inference(forward_demodulation,[],[f129,f153]) ).
fof(f2126,plain,
! [X0] : '==>'('0',X0) = X0,
inference(forward_demodulation,[],[f2125,f26]) ).
fof(f3772,plain,
! [X2,X0,X1] : '>='('==>'(X0,X1),'==>'(X0,'==>'(X2,X1))),
inference(forward_demodulation,[],[f187,f2126]) ).
fof(f3797,plain,
! [X0] : '>='(sK0,'==>'(sK0,'==>'(X0,sK1))),
inference(superposition,[],[f3772,f38]) ).
fof(f9961,plain,
! [X0] : '>='('+'('==>'(X0,sK2),sK2),'==>'(X0,sK1)),
inference(resolution,[],[f449,f164]) ).
fof(f9964,plain,
! [X0] : '>='('+'('==>'(X0,sK0),sK0),'==>'(X0,sK1)),
inference(resolution,[],[f449,f163]) ).
fof(f10067,plain,
! [X0] : '>='('+'(sK0,'==>'(X0,sK0)),'==>'(X0,sK1)),
inference(forward_demodulation,[],[f9964,f25]) ).
fof(f10070,plain,
! [X0] : '>='('+'(sK2,'==>'(X0,sK2)),'==>'(X0,sK1)),
inference(forward_demodulation,[],[f9961,f25]) ).
fof(f13382,plain,
'>='(sK0,'==>'(sK0,sK2)),
inference(superposition,[],[f3797,f37]) ).
fof(f15057,plain,
'0' = '==>'(sK0,'==>'(sK0,sK2)),
inference(resolution,[],[f13382,f193]) ).
fof(f43298,plain,
! [X0] : '>='(X0,'==>'('+'('==>'(X0,sK0),'==>'('==>'(sK0,X0),sK0)),sK1)),
inference(resolution,[],[f832,f163]) ).
fof(f43952,plain,
! [X0] : '>='('+'('==>'(X0,sK0),'==>'('==>'(sK0,X0),sK0)),'==>'(X0,sK1)),
inference(resolution,[],[f836,f163]) ).
fof(f167416,plain,
'>='('+'(sK0,'==>'(sK2,sK0)),sK2),
inference(superposition,[],[f10067,f37]) ).
fof(f167508,plain,
'>='('+'(sK2,'==>'(sK0,sK2)),sK0),
inference(superposition,[],[f10070,f38]) ).
fof(f167789,plain,
'>='('==>'(sK2,sK0),'==>'(sK0,sK2)),
inference(resolution,[],[f167416,f31]) ).
fof(f167865,plain,
'>='('==>'(sK0,sK2),'==>'(sK2,sK0)),
inference(resolution,[],[f167508,f31]) ).
fof(f194301,plain,
( ~ '>='('==>'(sK0,sK2),'==>'(sK2,sK0))
| '==>'(sK2,sK0) = '==>'(sK0,sK2) ),
inference(resolution,[],[f167789,f29]) ).
fof(f194337,definition,
( spl3_39
<=> '==>'(sK2,sK0) = '==>'(sK0,sK2) ),
introduced(definition,[new_symbols(definition,[spl3_39])],[avatar_definition]) ).
fof(f194339,plain,
( '==>'(sK2,sK0) = '==>'(sK0,sK2)
| ~ spl3_39 ),
inference(avatar_component_clause,[],[f194337]) ).
fof(f194341,definition,
( spl3_40
<=> '>='('==>'(sK0,sK2),'==>'(sK2,sK0)) ),
introduced(definition,[new_symbols(definition,[spl3_40])],[avatar_definition]) ).
fof(f194344,plain,
( spl3_39
| ~ spl3_40 ),
inference(avatar_split_clause,[],[f194301,f194341,f194337]) ).
fof(f197281,plain,
spl3_40,
inference(avatar_split_clause,[],[f167865,f194341]) ).
fof(f256895,plain,
( '>='(sK2,'==>'('+'('==>'(sK0,sK2),'==>'('==>'(sK0,sK2),sK0)),sK1))
| ~ spl3_39 ),
inference(superposition,[],[f43298,f194339]) ).
fof(f256897,plain,
( '>='('+'('==>'(sK0,sK2),'==>'('==>'(sK0,sK2),sK0)),'==>'(sK2,sK1))
| ~ spl3_39 ),
inference(superposition,[],[f43952,f194339]) ).
fof(f257081,definition,
( spl3_45
<=> '>='(sK2,sK0) ),
introduced(definition,[new_symbols(definition,[spl3_45])],[avatar_definition]) ).
fof(f257082,plain,
( '>='(sK2,sK0)
| ~ spl3_45 ),
inference(avatar_component_clause,[],[f257081]) ).
fof(f257156,plain,
( '>='('+'('==>'(sK0,sK2),'==>'('==>'(sK0,sK2),sK0)),sK2)
| ~ spl3_39 ),
inference(forward_demodulation,[],[f256897,f37]) ).
fof(f257157,plain,
( '>='(sK2,'==>'('+'(sK0,'==>'(sK0,'==>'(sK0,sK2))),sK1))
| ~ spl3_39 ),
inference(forward_demodulation,[],[f256895,f36]) ).
fof(f257166,plain,
( '>='('+'(sK0,'==>'(sK0,'==>'(sK0,sK2))),sK2)
| ~ spl3_39 ),
inference(forward_demodulation,[],[f257156,f36]) ).
fof(f257167,plain,
( '>='(sK2,'==>'('+'(sK0,'0'),sK1))
| ~ spl3_39 ),
inference(forward_demodulation,[],[f257157,f15057]) ).
fof(f257172,plain,
( '>='('+'(sK0,'0'),sK2)
| ~ spl3_39 ),
inference(forward_demodulation,[],[f257166,f15057]) ).
fof(f257173,plain,
( '>='(sK2,'==>'(sK0,sK1))
| ~ spl3_39 ),
inference(forward_demodulation,[],[f257167,f26]) ).
fof(f257175,plain,
( '>='(sK0,sK2)
| ~ spl3_39 ),
inference(forward_demodulation,[],[f257172,f26]) ).
fof(f257176,plain,
( '>='(sK2,sK0)
| ~ spl3_39 ),
inference(forward_demodulation,[],[f257173,f38]) ).
fof(f257178,plain,
( spl3_45
| ~ spl3_39 ),
inference(avatar_split_clause,[],[f257176,f194337,f257081]) ).
fof(f259693,plain,
( ~ '>='(sK2,sK0)
| sK0 = sK2
| ~ spl3_39 ),
inference(resolution,[],[f257175,f29]) ).
fof(f259731,plain,
( sK0 = sK2
| ~ spl3_39
| ~ spl3_45 ),
inference(forward_subsumption_resolution,[],[f259693,f257082]) ).
fof(f259734,plain,
( $false
| ~ spl3_39
| ~ spl3_45 ),
inference(forward_subsumption_resolution,[],[f259731,f39]) ).
fof(f259735,plain,
( ~ spl3_39
| ~ spl3_45 ),
inference(avatar_contradiction_clause,[],[f259734]) ).
cnf(s31,plain,
( spl3_39
| ~ spl3_40 ),
inference(sat_conversion,[],[f194344]) ).
cnf(s33,plain,
spl3_40,
inference(sat_conversion,[],[f197281]) ).
cnf(s48,plain,
( ~ spl3_39
| spl3_45 ),
inference(sat_conversion,[],[f257178]) ).
cnf(s49,plain,
( ~ spl3_39
| ~ spl3_45 ),
inference(sat_conversion,[],[f259735]) ).
cnf(s50,plain,
spl3_39,
inference(rat,[],[s31,s33]) ).
cnf(s51,plain,
~ spl3_45,
inference(rat,[],[s49,s50]) ).
cnf(s52,plain,
$false,
inference(rat,[],[s48,s51,s50]) ).
fof(f259736,plain,
$false,
inference(avatar_sat_refutation,[],[s52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL888+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.42 % Computer : n003.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 27 17:06:11 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.21/0.47 Running first-order model finding
% 0.21/0.47 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 44.98/6.88 % (788783)Will run a generic schedule for satisfiability detection.
% 44.98/6.88 % (788792)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3014298021:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 44.98/6.88 % (788788)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1091215288_2999 on theBenchmark for (2999ds/0Mi)
% 44.98/6.88 % TRYING [1]
% 44.98/6.88 % TRYING [2]
% 44.98/6.88 % TRYING [3]
% 44.98/6.88 % (788789)% WARNING: option uhcvi not known.
% 44.98/6.88 % TRYING [4]
% 44.98/6.88 % (788789)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1786897389:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 44.98/6.88 % (788791)dis+10_1_sil=32000:sp=arity:random_seed=491275268:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 44.98/6.88 % (788790)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3113110383:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 44.98/6.88 % (788793)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3322982592:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 44.98/6.88 % (788794)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3167286005:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 44.98/6.88 % TRYING [5]
% 44.98/6.88 % TRYING [6]
% 44.98/6.88 % (788792)Instruction limit reached!
% 44.98/6.88 % (788792)------------------------------
% 44.98/6.88 % (788792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.98/6.88 % (788792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.98/6.88 % (788792)CaDiCaL version: 2.1.3
% 44.98/6.88 % (788792)Termination reason: Instruction limit
% 44.98/6.88 % (788792)Termination phase: Saturation
% 44.98/6.88 % (788792)Time elapsed: 0.060 s
% 44.98/6.88 % (788792)Peak memory usage: 12 MB
% 44.98/6.88 % (788792)Instructions burned: 118 (million)
% 44.98/6.88 % (788802)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3838924391:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 44.98/6.88 % TRYING [1]
% 44.98/6.88 % TRYING [2]
% 44.98/6.88 % TRYING [3]
% 44.98/6.88 % TRYING [4]
% 44.98/6.88 % TRYING [5]
% 44.98/6.88 % (788791)Instruction limit reached!
% 44.98/6.88 % (788791)------------------------------
% 44.98/6.88 % (788791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.98/6.88 % (788791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.98/6.88 % (788791)CaDiCaL version: 2.1.3
% 44.98/6.88 % (788791)Termination reason: Instruction limit
% 44.98/6.88 % (788791)Termination phase: Saturation
% 44.98/6.88 % (788791)Time elapsed: 0.107 s
% 44.98/6.88 % (788791)Peak memory usage: 12 MB
% 44.98/6.88 % (788791)Instructions burned: 103 (million)
% 44.98/6.88 % TRYING [6]
% 44.98/6.88 % (788804)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1200901432:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 44.98/6.88 % (788793)Instruction limit reached!
% 44.98/6.88 % (788793)------------------------------
% 44.98/6.88 % (788793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.98/6.88 % (788793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.98/6.88 % (788793)CaDiCaL version: 2.1.3
% 44.98/6.88 % (788793)Termination reason: Instruction limit
% 44.98/6.88 % (788793)Termination phase: Saturation
% 44.98/6.88 % (788793)Time elapsed: 0.136 s
% 44.98/6.88 % (788793)Peak memory usage: 13 MB
% 44.98/6.88 % (788793)Instructions burned: 131 (million)
% 44.98/6.88 % (788806)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=1606127230:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 44.98/6.89 % (788794)Instruction limit reached!
% 44.98/6.89 % (788794)------------------------------
% 44.98/6.89 % (788794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.98/6.89 % (788794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.98/6.89 % (788794)CaDiCaL version: 2.1.3
% 44.98/6.89 % (788794)Termination reason: Instruction limit
% 44.98/6.89 % (788794)Termination phase: Saturation
% 44.98/6.89 % (788794)Time elapsed: 0.188 s
% 44.98/6.89 % (788794)Peak memory usage: 13 MB
% 44.98/6.89 % (788794)Instructions burned: 159 (million)
% 44.98/6.89 % TRYING [7]
% 44.98/6.89 % (788804)Instruction limit reached!
% 44.98/6.89 % (788804)------------------------------
% 44.98/6.89 % (788804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.98/6.89 % (788804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.98/6.89 % (788804)CaDiCaL version: 2.1.3
% 84.77/12.41 % (788804)Termination reason: Instruction limit
% 84.77/12.41 % (788804)Termination phase: Saturation
% 84.77/12.41 % (788804)Time elapsed: 0.077 s
% 84.77/12.41 % (788804)Peak memory usage: 14 MB
% 84.77/12.41 % (788804)Instructions burned: 131 (million)
% 84.77/12.41 % TRYING [7]
% 84.77/12.41 % (788808)ott-21_1_sil=16000:fs=off:random_seed=3958320933:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 84.77/12.41 % (788809)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2788381494:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 84.77/12.41 % (788808)Instruction limit reached!
% 84.77/12.41 % (788808)------------------------------
% 84.77/12.41 % (788808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.77/12.41 % (788808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.77/12.41 % (788808)CaDiCaL version: 2.1.3
% 84.77/12.41 % (788808)Termination reason: Instruction limit
% 84.77/12.41 % (788808)Termination phase: Saturation
% 84.77/12.41 % (788808)Time elapsed: 0.135 s
% 84.77/12.41 % (788808)Peak memory usage: 12 MB
% 84.77/12.41 % (788808)Instructions burned: 180 (million)
% 84.77/12.41 % (788812)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1576679474:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 84.77/12.41 % TRYING [1]
% 84.77/12.41 % TRYING [2]
% 84.77/12.41 % TRYING [3]
% 84.77/12.41 % TRYING [8]
% 84.77/12.41 % TRYING [4]
% 84.77/12.41 % TRYING [5]
% 84.77/12.41 % TRYING [6]
% 84.77/12.41 % (788809)Instruction limit reached!
% 84.77/12.41 % (788809)------------------------------
% 84.77/12.41 % (788809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.77/12.41 % (788809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.77/12.41 % (788809)CaDiCaL version: 2.1.3
% 84.77/12.41 % (788809)Termination reason: Instruction limit
% 84.77/12.41 % (788809)Termination phase: Saturation
% 84.77/12.41 % (788809)Time elapsed: 0.273 s
% 84.77/12.41 % (788809)Peak memory usage: 14 MB
% 84.77/12.41 % (788809)Instructions burned: 478 (million)
% 84.77/12.41 % (788802)Instruction limit reached!
% 84.77/12.41 % (788802)------------------------------
% 84.77/12.41 % (788802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.77/12.41 % (788802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.77/12.41 % (788802)CaDiCaL version: 2.1.3
% 84.77/12.41 % (788802)Termination reason: Instruction limit
% 84.77/12.41 % (788802)Termination phase: Finite model building constraint generation
% 84.77/12.41 % (788802)Time elapsed: 0.457 s
% 84.77/12.41 % (788802)Peak memory usage: 26 MB
% 84.77/12.41 % (788802)Instructions burned: 714 (million)
% 84.77/12.41 % (788816)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4054044891:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 84.77/12.41 % (788815)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=562323471:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 84.77/12.41 % TRYING [14]
% 84.77/12.41 % TRYING [7]
% 84.77/12.41 % TRYING [8]
% 84.77/12.41 % (788806)Instruction limit reached!
% 84.77/12.41 % (788806)------------------------------
% 84.77/12.41 % (788806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.77/12.41 % (788806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.77/12.41 % (788806)CaDiCaL version: 2.1.3
% 84.77/12.41 % (788806)Termination reason: Instruction limit
% 84.77/12.41 % (788806)Termination phase: Saturation
% 84.77/12.41 % (788806)Time elapsed: 0.655 s
% 84.77/12.41 % (788806)Peak memory usage: 17 MB
% 84.77/12.41 % (788806)Instructions burned: 684 (million)
% 84.77/12.41 % (788820)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=1958254949:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 84.77/12.41 % (788812)Instruction limit reached!
% 84.77/12.41 % (788812)------------------------------
% 84.77/12.41 % (788812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.77/12.41 % (788812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.77/12.41 % (788812)CaDiCaL version: 2.1.3
% 84.77/12.41 % (788812)Termination reason: Instruction limit
% 84.77/12.41 % (788812)Termination phase: Finite model building SAT solving
% 84.77/12.41 % (788812)Time elapsed: 0.529 s
% 84.77/12.41 % (788812)Peak memory usage: 21 MB
% 84.77/12.41 % (788812)Instructions burned: 866 (million)
% 84.77/12.41 % (788822)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1032672349:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 84.77/12.41 % (788815)Instruction limit reached!
% 84.77/12.41 % (788815)------------------------------
% 102.47/15.02 % (788815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788815)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788815)Termination reason: Instruction limit
% 102.47/15.02 % (788815)Termination phase: Saturation
% 102.47/15.02 % (788815)Time elapsed: 0.629 s
% 102.47/15.02 % (788815)Peak memory usage: 23 MB
% 102.47/15.02 % (788815)Instructions burned: 1180 (million)
% 102.47/15.02 % (788816)Instruction limit reached!
% 102.47/15.02 % (788816)------------------------------
% 102.47/15.02 % (788816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788816)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788816)Termination reason: Instruction limit
% 102.47/15.02 % (788816)Termination phase: Finite model building constraint generation
% 102.47/15.02 % (788816)Time elapsed: 0.641 s
% 102.47/15.02 % (788816)Peak memory usage: 80 MB
% 102.47/15.02 % (788816)Instructions burned: 890 (million)
% 102.47/15.02 % (788825)fmb+10_1_sil=64000:random_seed=1900923520:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 102.47/15.02 % TRYING [1]
% 102.47/15.02 % TRYING [2]
% 102.47/15.02 % TRYING [3]
% 102.47/15.02 % TRYING [4]
% 102.47/15.02 % TRYING [5]
% 102.47/15.02 % (788828)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1826420303:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi)
% 102.47/15.02 % TRYING [20]
% 102.47/15.02 % TRYING [6]
% 102.47/15.02 % TRYING [7]
% 102.47/15.02 % (788820)Instruction limit reached!
% 102.47/15.02 % (788820)------------------------------
% 102.47/15.02 % (788820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788820)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788820)Termination reason: Instruction limit
% 102.47/15.02 % (788820)Termination phase: Saturation
% 102.47/15.02 % (788820)Time elapsed: 0.683 s
% 102.47/15.02 % (788820)Peak memory usage: 17 MB
% 102.47/15.02 % (788820)Instructions burned: 693 (million)
% 102.47/15.02 % (788830)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=531111161:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 102.47/15.02 % TRYING [8]
% 102.47/15.02 % TRYING [8]
% 102.47/15.02 % (788822)Instruction limit reached!
% 102.47/15.02 % (788822)------------------------------
% 102.47/15.02 % (788822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788822)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788822)Termination reason: Instruction limit
% 102.47/15.02 % (788822)Termination phase: Saturation
% 102.47/15.02 % (788822)Time elapsed: 0.830 s
% 102.47/15.02 % (788822)Peak memory usage: 18 MB
% 102.47/15.02 % (788822)Instructions burned: 879 (million)
% 102.47/15.02 % (788832)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2350677779:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 102.47/15.02 % TRYING [9]
% 102.47/15.02 % TRYING [9]
% 102.47/15.02 % (788830)Instruction limit reached!
% 102.47/15.02 % (788830)------------------------------
% 102.47/15.02 % (788830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788830)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788830)Termination reason: Instruction limit
% 102.47/15.02 % (788830)Termination phase: Finite model building SAT solving
% 102.47/15.02 % (788830)Time elapsed: 0.772 s
% 102.47/15.02 % (788830)Peak memory usage: 42 MB
% 102.47/15.02 % (788830)Instructions burned: 920 (million)
% 102.47/15.02 % (788835)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1176626884:i=1472:ins=7:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/1472Mi)
% 102.47/15.02 % (788835)Instruction limit reached!
% 102.47/15.02 % (788835)------------------------------
% 102.47/15.02 % (788835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788835)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788835)Termination reason: Instruction limit
% 102.47/15.02 % (788835)Termination phase: Saturation
% 102.47/15.02 % (788835)Time elapsed: 1.247 s
% 102.47/15.02 % (788835)Peak memory usage: 21 MB
% 102.47/15.02 % (788835)Instructions burned: 1473 (million)
% 102.47/15.02 % TRYING [10]
% 102.47/15.02 % (788838)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2569040795:i=6324_2963 on theBenchmark for (2963ds/6324Mi)
% 102.47/15.02 % TRYING [77]
% 102.47/15.02 % (788832)Instruction limit reached!
% 102.47/15.02 % (788832)------------------------------
% 102.47/15.02 % (788832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788832)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788832)Termination reason: Instruction limit
% 102.47/15.02 % (788832)Termination phase: Saturation
% 102.47/15.02 % (788832)Time elapsed: 4.579 s
% 102.47/15.02 % (788832)Peak memory usage: 37 MB
% 102.47/15.02 % (788832)Instructions burned: 5131 (million)
% 102.47/15.02 % (788842)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1072895711:fmbsr=2.30978:i=2174_2935 on theBenchmark for (2935ds/2174Mi)
% 102.47/15.02 % TRYING [16]
% 102.47/15.02 % TRYING [10]
% 102.47/15.02 % (788842)Instruction limit reached!
% 102.47/15.02 % (788842)------------------------------
% 102.47/15.02 % (788842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788842)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788842)Termination reason: Instruction limit
% 102.47/15.02 % (788842)Termination phase: Finite model building constraint generation
% 102.47/15.02 % (788842)Time elapsed: 1.463 s
% 102.47/15.02 % (788842)Peak memory usage: 132 MB
% 102.47/15.02 % (788842)Instructions burned: 2175 (million)
% 102.47/15.02 % (788846)ott-2_1_sil=16000:newcnf=on:random_seed=1605172848:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2920 on theBenchmark for (2920ds/869Mi)
% 102.47/15.02 % (788828)Instruction limit reached!
% 102.47/15.02 % (788828)------------------------------
% 102.47/15.02 % (788828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788828)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788828)Termination reason: Instruction limit
% 102.47/15.02 % (788828)Termination phase: Finite model building constraint generation
% 102.47/15.02 % (788828)Time elapsed: 7.103 s
% 102.47/15.02 % (788828)Peak memory usage: 661 MB
% 102.47/15.02 % (788828)Instructions burned: 9516 (million)
% 102.47/15.02 % (788838)Instruction limit reached!
% 102.47/15.02 % (788838)------------------------------
% 102.47/15.02 % (788838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788838)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788838)Termination reason: Instruction limit
% 102.47/15.02 % (788838)Termination phase: Finite model building constraint generation
% 102.47/15.02 % (788838)Time elapsed: 4.713 s
% 102.47/15.02 % (788838)Peak memory usage: 420 MB
% 102.47/15.02 % (788838)Instructions burned: 6325 (million)
% 102.47/15.02 % (788849)ott+10_1_sil=32000:tgt=ground:random_seed=319522801:i=5114:av=off_2914 on theBenchmark for (2914ds/5114Mi)
% 102.47/15.02 % (788850)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2052604759:i=54282_2914 on theBenchmark for (2914ds/54282Mi)
% 102.47/15.02 % TRYING [1]
% 102.47/15.02 % TRYING [2]
% 102.47/15.02 % TRYING [3]
% 102.47/15.02 % TRYING [4]
% 102.47/15.02 % TRYING [5]
% 102.47/15.02 % TRYING [6]
% 102.47/15.02 % TRYING [7]
% 102.47/15.02 % (788846)Instruction limit reached!
% 102.47/15.02 % (788846)------------------------------
% 102.47/15.02 % (788846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788846)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788846)Termination reason: Instruction limit
% 102.47/15.02 % (788846)Termination phase: Saturation
% 102.47/15.02 % (788846)Time elapsed: 0.883 s
% 102.47/15.02 % (788846)Peak memory usage: 17 MB
% 102.47/15.02 % (788846)Instructions burned: 870 (million)
% 102.47/15.02 % (788854)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1021521971:i=3512:aac=none_2911 on theBenchmark for (2911ds/3512Mi)
% 102.47/15.02 % TRYING [8]
% 102.47/15.02 % TRYING [9]
% 102.47/15.02 % (788825)Instruction limit reached!
% 102.47/15.02 % (788825)------------------------------
% 102.47/15.02 % (788825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788825)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788825)Termination reason: Instruction limit
% 102.47/15.02 % (788825)Termination phase: Finite model building SAT solving
% 102.47/15.02 % (788825)Time elapsed: 9.564 s
% 102.47/15.02 % (788825)Peak memory usage: 71 MB
% 102.47/15.02 % (788825)Instructions burned: 22062 (million)
% 102.47/15.02 % (788856)dis+21_1_sil=32000:sas=cadical:random_seed=1189828298:i=3773:amm=off_2891 on theBenchmark for (2891ds/3773Mi)
% 102.47/15.02 % (788854)Instruction limit reached!
% 102.47/15.02 % (788854)------------------------------
% 102.47/15.02 % (788854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788854)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788854)Termination reason: Instruction limit
% 102.47/15.02 % (788854)Termination phase: Saturation
% 102.47/15.02 % (788854)Time elapsed: 3.041 s
% 102.47/15.02 % (788854)Peak memory usage: 28 MB
% 102.47/15.02 % (788854)Instructions burned: 3513 (million)
% 102.47/15.02 % (788860)ott+11_1_sil=16000:gs=on:random_seed=3861139819:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2880 on theBenchmark for (2880ds/2251Mi)
% 102.47/15.02 % (788856)Instruction limit reached!
% 102.47/15.02 % (788856)------------------------------
% 102.47/15.02 % (788856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788856)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788856)Termination reason: Instruction limit
% 102.47/15.02 % (788856)Termination phase: Saturation
% 102.47/15.02 % (788856)Time elapsed: 1.789 s
% 102.47/15.02 % (788856)Peak memory usage: 31 MB
% 102.47/15.02 % (788856)Instructions burned: 3775 (million)
% 102.47/15.02 % (788862)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3056079933:fmbsr=1.6:i=67534_2873 on theBenchmark for (2873ds/67534Mi)
% 102.47/15.02 % TRYING [7]
% 102.47/15.02 % TRYING [8]
% 102.47/15.02 % (788849)Instruction limit reached!
% 102.47/15.02 % (788849)------------------------------
% 102.47/15.02 % (788849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788849)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788849)Termination reason: Instruction limit
% 102.47/15.02 % (788849)Termination phase: Saturation
% 102.47/15.02 % (788849)Time elapsed: 4.643 s
% 102.47/15.02 % (788849)Peak memory usage: 36 MB
% 102.47/15.02 % (788849)Instructions burned: 5115 (million)
% 102.47/15.02 % (788942)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1195477868:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2867 on theBenchmark for (2867ds/4591Mi)
% 102.47/15.02 % TRYING [9]
% 102.47/15.02 % (788860)Instruction limit reached!
% 102.47/15.02 % (788860)------------------------------
% 102.47/15.02 % (788860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788860)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788860)Termination reason: Instruction limit
% 102.47/15.02 % (788860)Termination phase: Saturation
% 102.47/15.02 % (788860)Time elapsed: 1.525 s
% 102.47/15.02 % (788860)Peak memory usage: 26 MB
% 102.47/15.02 % (788860)Instructions burned: 2253 (million)
% 102.47/15.02 % (789008)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3646233078:i=29340_2864 on theBenchmark for (2864ds/29340Mi)
% 102.47/15.02 % (788789) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-788783-788789"...
% 102.47/15.02 % (788789)...printing done.
% 102.47/15.02 % (788789)Refutation found. Thanks to Tanya!
% 102.47/15.02 % SZS status Theorem for theBenchmark
% 102.47/15.02 % SZS output start Proof for theBenchmark
% See solution above
% 102.47/15.02 % (788789)------------------------------
% 102.47/15.02 % (788789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.47/15.02 % (788789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.47/15.02 % (788789)CaDiCaL version: 2.1.3
% 102.47/15.02 % (788789)Termination reason: Refutation
% 102.47/15.02 % (788789)Time elapsed: 14.468 s
% 102.47/15.02 % (788789)Peak memory usage: 130 MB
% 102.47/15.02 % (788789)Instructions burned: 17094 (million)
% 102.47/15.02 % (788783)Success in time 14.54 s
% 102.47/15.02 % Vampire exiting
%------------------------------------------------------------------------------