%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP748-4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 10:18:42 AM UTC 2026
% Result : Unsatisfiable 55.18s 8.25s
% Output : Refutation 55.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 17
% Syntax : Number of formulae : 103 ( 96 unt; 6 def)
% Number of atoms : 110 ( 109 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 3 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 143 ( 143 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(mult(mult(X0,X1),X2),X1) = mult(X0,mult(mult(X1,X2),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f07) ).
fof(f8,axiom,
! [X0,X1] : mult(mult(X0,X1),i(X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f08) ).
fof(f9,axiom,
! [X0] : mult(X0,i(X0)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f09) ).
fof(f10,plain,
! [X0] : unit = mult(X0,i(X0)),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0] : mult(i(X0),X0) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f10) ).
fof(f12,plain,
! [X0] : unit = mult(i(X0),X0),
inference(reorient_equations,[],[f11]) ).
fof(f13,axiom,
! [X0,X1] :
( mult(i(X0),mult(X0,X1)) = X1
| mult(X0,X1) = mult(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f11) ).
fof(f14,negated_conjecture,
mult(mult(a,b),mult(c,a)) != mult(mult(a,mult(b,c)),a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f15,definition,
sF0 = mult(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f16,plain,
mult(a,b) = sF0,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF1 = mult(c,a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f18,plain,
mult(c,a) = sF1,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF2 = mult(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f20,plain,
mult(sF0,sF1) = sF2,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF3 = mult(b,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f22,plain,
mult(b,c) = sF3,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF4 = mult(a,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f24,plain,
mult(a,sF3) = sF4,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF5 = mult(sF4,a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f26,plain,
mult(sF4,a) = sF5,
inference(reorient_equations,[],[f25]) ).
fof(f27,plain,
sF2 != sF5,
inference(definition_folding,[],[f14,f26,f24,f22,f20,f18,f16]) ).
fof(f54,plain,
! [X0] : rd(unit,i(X0)) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f57,plain,
! [X0] : i(X0) = rd(unit,X0),
inference(superposition,[],[f4,f12]) ).
fof(f60,plain,
b = rd(sF3,c),
inference(superposition,[],[f4,f22]) ).
fof(f64,plain,
! [X0] : i(i(X0)) = X0,
inference(forward_demodulation,[],[f54,f57]) ).
fof(f70,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,i(X1)),
inference(superposition,[],[f8,f3]) ).
fof(f74,plain,
a = mult(sF4,i(sF3)),
inference(superposition,[],[f8,f24]) ).
fof(f80,plain,
! [X0,X1] : mult(X0,X1) = rd(X0,i(X1)),
inference(superposition,[],[f4,f8]) ).
fof(f81,plain,
! [X0,X1] : i(X1) = ld(mult(X0,X1),X0),
inference(superposition,[],[f2,f8]) ).
fof(f89,plain,
! [X0,X1] : mult(X0,mult(mult(i(X0),X1),i(X0))) = mult(mult(unit,X1),i(X0)),
inference(superposition,[],[f7,f10]) ).
fof(f91,plain,
! [X2,X0,X1] : mult(mult(X0,X1),mult(mult(i(X1),X2),i(X1))) = mult(mult(X0,X2),i(X1)),
inference(superposition,[],[f7,f8]) ).
fof(f95,plain,
! [X0,X1] : mult(i(X0),mult(mult(X0,X1),X0)) = mult(mult(unit,X1),X0),
inference(superposition,[],[f7,f12]) ).
fof(f99,plain,
! [X0] : mult(c,mult(mult(a,X0),a)) = mult(mult(sF1,X0),a),
inference(superposition,[],[f7,f18]) ).
fof(f105,plain,
! [X0,X1] : mult(unit,X1) = mult(X0,mult(mult(X1,i(mult(X0,X1))),X1)),
inference(superposition,[],[f7,f10]) ).
fof(f117,plain,
! [X0,X1] : mult(unit,X1) = mult(X0,mult(rd(X1,mult(X0,X1)),X1)),
inference(forward_demodulation,[],[f105,f70]) ).
fof(f120,plain,
! [X0,X1] : mult(X1,X0) = mult(i(X0),mult(mult(X0,X1),X0)),
inference(forward_demodulation,[],[f95,f6]) ).
fof(f121,plain,
! [X2,X0,X1] : mult(mult(X0,X1),mult(mult(i(X1),X2),i(X1))) = rd(mult(X0,X2),X1),
inference(forward_demodulation,[],[f91,f70]) ).
fof(f122,plain,
! [X0,X1] : mult(X0,mult(mult(i(X0),X1),i(X0))) = rd(mult(unit,X1),X0),
inference(forward_demodulation,[],[f89,f70]) ).
fof(f126,plain,
! [X0,X1] : mult(X0,mult(rd(X1,mult(X0,X1)),X1)) = X1,
inference(forward_demodulation,[],[f117,f6]) ).
fof(f127,plain,
! [X2,X0,X1] : rd(mult(X0,X2),X1) = mult(mult(X0,X1),rd(mult(i(X1),X2),X1)),
inference(forward_demodulation,[],[f121,f70]) ).
fof(f128,plain,
! [X0,X1] : mult(X0,mult(mult(i(X0),X1),i(X0))) = rd(X1,X0),
inference(forward_demodulation,[],[f122,f6]) ).
fof(f130,plain,
! [X0,X1] : rd(X1,X0) = mult(X0,rd(mult(i(X0),X1),X0)),
inference(forward_demodulation,[],[f128,f70]) ).
fof(f135,plain,
! [X0,X1] :
( mult(ld(X1,X0),X1) = X0
| ld(X1,X0) = mult(i(X1),X0) ),
inference(superposition,[],[f13,f1]) ).
fof(f151,plain,
! [X0,X1] :
( mult(X1,X0) = ld(i(X1),X0)
| mult(X0,X1) = mult(X1,X0) ),
inference(superposition,[],[f2,f13]) ).
fof(f203,plain,
i(sF3) = ld(sF4,a),
inference(superposition,[],[f2,f74]) ).
fof(f306,plain,
! [X0,X1] : i(X1) = ld(X0,rd(X0,X1)),
inference(superposition,[],[f2,f70]) ).
fof(f358,plain,
! [X0,X1] : ld(X0,X1) = i(ld(X1,X0)),
inference(superposition,[],[f81,f1]) ).
fof(f477,plain,
! [X0,X1] : mult(rd(X0,X1),mult(rd(X1,X0),X1)) = X1,
inference(superposition,[],[f126,f3]) ).
fof(f490,plain,
a = mult(sF4,mult(rd(a,sF5),a)),
inference(superposition,[],[f126,f26]) ).
fof(f497,plain,
! [X0,X1] : ld(X1,X0) = mult(rd(X0,mult(X1,X0)),X0),
inference(superposition,[],[f2,f126]) ).
fof(f502,plain,
! [X0,X1] : ld(X0,X1) = i(mult(rd(X0,mult(X1,X0)),X0)),
inference(superposition,[],[f81,f126]) ).
fof(f773,plain,
! [X0,X1] : mult(mult(X1,X0),X1) = ld(i(X1),mult(X0,X1)),
inference(superposition,[],[f2,f120]) ).
fof(f880,plain,
! [X0,X1] : i(rd(mult(i(X1),X0),X1)) = ld(rd(X0,X1),X1),
inference(superposition,[],[f81,f130]) ).
fof(f1069,plain,
! [X0] : mult(mult(sF1,i(X0)),a) = mult(c,mult(rd(a,X0),a)),
inference(superposition,[],[f99,f70]) ).
fof(f1084,plain,
! [X0] : mult(c,mult(rd(a,X0),a)) = mult(rd(sF1,X0),a),
inference(forward_demodulation,[],[f1069,f70]) ).
fof(f2061,plain,
ld(sF4,a) = mult(rd(a,sF5),a),
inference(superposition,[],[f2,f490]) ).
fof(f2081,plain,
i(sF3) = mult(rd(a,sF5),a),
inference(forward_demodulation,[],[f2061,f203]) ).
fof(f2112,plain,
! [X0,X1] :
( ld(X1,X0) = mult(i(X1),X0)
| rd(X0,X1) = ld(X1,X0) ),
inference(superposition,[],[f4,f135]) ).
fof(f2399,plain,
! [X0,X1] :
( ld(X0,X1) = mult(i(X0),X1)
| mult(i(X0),X1) = mult(X1,i(X0)) ),
inference(superposition,[],[f151,f64]) ).
fof(f2417,plain,
! [X0,X1] :
( mult(i(X0),X1) = rd(X1,X0)
| ld(X0,X1) = mult(i(X0),X1) ),
inference(forward_demodulation,[],[f2399,f70]) ).
fof(f2503,plain,
! [X2,X0,X1] : mult(mult(X1,X2),rd(X0,X2)) = rd(mult(X1,ld(i(X2),X0)),X2),
inference(superposition,[],[f127,f1]) ).
fof(f2528,plain,
! [X2,X0,X1] : i(rd(mult(i(X2),X1),X2)) = ld(rd(mult(X0,X1),X2),mult(X0,X2)),
inference(superposition,[],[f81,f127]) ).
fof(f2547,plain,
! [X2,X0,X1] : ld(rd(mult(X0,X1),X2),mult(X0,X2)) = ld(rd(X1,X2),X2),
inference(forward_demodulation,[],[f2528,f880]) ).
fof(f5992,plain,
! [X0,X1] : mult(rd(X0,X1),X0) = ld(rd(X1,X0),X0),
inference(superposition,[],[f2,f477]) ).
fof(f5997,plain,
! [X0,X1] : ld(X0,rd(X1,X0)) = i(mult(rd(X0,X1),X0)),
inference(superposition,[],[f81,f477]) ).
fof(f6171,plain,
! [X0,X1] : rd(X1,mult(X0,X1)) = rd(ld(X0,X1),X1),
inference(superposition,[],[f4,f497]) ).
fof(f22859,plain,
mult(c,i(sF3)) = mult(rd(sF1,sF5),a),
inference(superposition,[],[f1084,f2081]) ).
fof(f22924,plain,
rd(c,sF3) = mult(rd(sF1,sF5),a),
inference(forward_demodulation,[],[f22859,f70]) ).
fof(f22953,plain,
rd(sF1,sF5) = rd(rd(c,sF3),a),
inference(superposition,[],[f4,f22924]) ).
fof(f83994,plain,
! [X0,X1] :
( ld(X0,X1) != rd(X1,X0)
| ld(X0,X1) = mult(i(X0),X1) ),
inference(equality_factoring,[],[f2417]) ).
fof(f84010,plain,
! [X0,X1] : ld(X0,X1) = mult(i(X0),X1),
inference(forward_subsumption_resolution,[],[f83994,f2112]) ).
fof(f84337,plain,
! [X2,X0,X1] : mult(ld(X0,X1),X2) = ld(ld(X1,X0),X2),
inference(superposition,[],[f84010,f358]) ).
fof(f84351,plain,
! [X0,X1] : mult(X0,X1) = ld(i(X0),X1),
inference(superposition,[],[f84010,f64]) ).
fof(f84607,plain,
! [X0,X1] : ld(X1,i(X0)) = i(mult(rd(X1,ld(X0,X1)),X1)),
inference(superposition,[],[f502,f84010]) ).
fof(f84610,plain,
! [X0,X1] : mult(mult(X1,i(X0)),X1) = ld(i(X1),ld(X0,X1)),
inference(superposition,[],[f773,f84010]) ).
fof(f84834,plain,
! [X0,X1] : mult(rd(X1,X0),X1) = ld(i(X1),ld(X0,X1)),
inference(forward_demodulation,[],[f84610,f70]) ).
fof(f84837,plain,
! [X0,X1] : ld(X1,i(X0)) = ld(X1,rd(ld(X0,X1),X1)),
inference(forward_demodulation,[],[f84607,f5997]) ).
fof(f84995,plain,
! [X0,X1] : mult(X1,ld(X0,X1)) = mult(rd(X1,X0),X1),
inference(forward_demodulation,[],[f84834,f84351]) ).
fof(f84997,plain,
! [X0,X1] : ld(X1,rd(X1,mult(X0,X1))) = ld(X1,i(X0)),
inference(forward_demodulation,[],[f84837,f6171]) ).
fof(f85081,plain,
! [X0,X1] : i(mult(X0,X1)) = ld(X1,i(X0)),
inference(forward_demodulation,[],[f84997,f306]) ).
fof(f85358,plain,
! [X2,X0,X1] : ld(rd(ld(i(X1),X2),X1),X1) = ld(mult(mult(X0,X1),rd(X2,X1)),mult(X0,X1)),
inference(superposition,[],[f2547,f2503]) ).
fof(f85413,plain,
! [X2,X1] : i(rd(X2,X1)) = ld(rd(ld(i(X1),X2),X1),X1),
inference(forward_demodulation,[],[f85358,f81]) ).
fof(f85538,plain,
! [X2,X1] : i(rd(X2,X1)) = mult(rd(X1,ld(i(X1),X2)),X1),
inference(forward_demodulation,[],[f85413,f5992]) ).
fof(f85633,plain,
! [X2,X1] : i(rd(X2,X1)) = mult(X1,ld(ld(i(X1),X2),X1)),
inference(forward_demodulation,[],[f85538,f84995]) ).
fof(f85691,plain,
! [X2,X1] : i(rd(X2,X1)) = mult(X1,mult(ld(X2,i(X1)),X1)),
inference(forward_demodulation,[],[f85633,f84337]) ).
fof(f85722,plain,
! [X2,X1] : i(rd(X2,X1)) = mult(X1,mult(i(mult(X1,X2)),X1)),
inference(forward_demodulation,[],[f85691,f85081]) ).
fof(f85745,plain,
! [X2,X1] : i(rd(X2,X1)) = mult(X1,ld(mult(X1,X2),X1)),
inference(forward_demodulation,[],[f85722,f84010]) ).
fof(f85766,plain,
! [X2,X1] : mult(X1,i(X2)) = i(rd(X2,X1)),
inference(forward_demodulation,[],[f85745,f81]) ).
fof(f85783,plain,
! [X2,X1] : rd(X1,X2) = i(rd(X2,X1)),
inference(forward_demodulation,[],[f85766,f70]) ).
fof(f89822,plain,
i(rd(sF1,sF5)) = rd(a,rd(c,sF3)),
inference(superposition,[],[f85783,f22953]) ).
fof(f89893,plain,
! [X2,X0,X1] : rd(X2,rd(X0,X1)) = mult(X2,rd(X1,X0)),
inference(superposition,[],[f80,f85783]) ).
fof(f89998,plain,
i(rd(sF1,sF5)) = mult(a,rd(sF3,c)),
inference(forward_demodulation,[],[f89822,f89893]) ).
fof(f90075,plain,
mult(a,b) = i(rd(sF1,sF5)),
inference(forward_demodulation,[],[f89998,f60]) ).
fof(f90113,plain,
mult(a,b) = rd(sF5,sF1),
inference(forward_demodulation,[],[f90075,f85783]) ).
fof(f90129,plain,
sF0 = rd(sF5,sF1),
inference(forward_demodulation,[],[f90113,f16]) ).
fof(f95213,plain,
mult(sF0,sF1) = sF5,
inference(superposition,[],[f3,f90129]) ).
fof(f95274,plain,
sF2 = sF5,
inference(forward_demodulation,[],[f95213,f20]) ).
fof(f95281,plain,
$false,
inference(forward_subsumption_resolution,[],[f95274,f27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP748-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 10:41:30 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.41 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
% 21.15/3.41 % (1843319)Will run a generic schedule for satisfiability detection.
% 21.15/3.41 % (1843325)% WARNING: option uhcvi not known.
% 21.15/3.41 % (1843330)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4234743896:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 21.15/3.41 % (1843328)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2404888985:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 21.15/3.41 % (1843327)dis+10_1_sil=32000:sp=arity:random_seed=3959963924:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 21.15/3.41 % (1843329)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1717471500:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 21.15/3.41 % (1843324)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3609049469_3000 on theBenchmark for (3000ds/0Mi)
% 21.15/3.41 % (1843325)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2660940460:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 21.15/3.41 % TRYING [1]
% 21.15/3.41 % TRYING [2]
% 21.15/3.41 % TRYING [3]
% 21.15/3.41 % TRYING [4]
% 21.15/3.41 % TRYING [5]
% 21.15/3.41 % (1843326)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1745967062:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 21.15/3.41 % TRYING [6]
% 21.15/3.41 % (1843327)Instruction limit reached!
% 21.15/3.41 % (1843327)------------------------------
% 21.15/3.41 % (1843327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.15/3.41 % (1843327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.41 % (1843327)CaDiCaL version: 2.1.3
% 21.15/3.41 % (1843327)Termination reason: Instruction limit
% 21.15/3.41 % (1843327)Termination phase: Saturation
% 21.15/3.41 % (1843327)Time elapsed: 0.082 s
% 21.15/3.41 % (1843327)Peak memory usage: 12 MB
% 21.15/3.41 % (1843327)Instructions burned: 104 (million)
% 21.15/3.41 % (1843328)Instruction limit reached!
% 21.15/3.41 % (1843328)------------------------------
% 21.15/3.41 % (1843328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.15/3.41 % (1843328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.41 % (1843328)CaDiCaL version: 2.1.3
% 21.15/3.41 % (1843328)Termination reason: Instruction limit
% 21.15/3.41 % (1843328)Termination phase: Saturation
% 21.15/3.41 % (1843328)Time elapsed: 0.100 s
% 21.15/3.41 % (1843328)Peak memory usage: 12 MB
% 21.15/3.41 % (1843328)Instructions burned: 117 (million)
% 21.15/3.41 % (1843329)Instruction limit reached!
% 21.15/3.41 % (1843329)------------------------------
% 21.15/3.41 % (1843329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.15/3.41 % (1843329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.41 % (1843329)CaDiCaL version: 2.1.3
% 21.15/3.41 % (1843329)Termination reason: Instruction limit
% 21.15/3.41 % (1843329)Termination phase: Saturation
% 21.15/3.41 % (1843329)Time elapsed: 0.115 s
% 21.15/3.41 % (1843329)Peak memory usage: 12 MB
% 21.15/3.41 % (1843329)Instructions burned: 131 (million)
% 21.15/3.41 % (1843338)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=616976989:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 21.15/3.41 % TRYING [1]
% 21.15/3.41 % TRYING [2]
% 21.15/3.41 % TRYING [3]
% 21.15/3.41 % TRYING [4]
% 21.15/3.41 % (1843339)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1213956594:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 21.15/3.41 % TRYING [5]
% 21.15/3.41 % (1843330)Instruction limit reached!
% 21.15/3.41 % (1843330)------------------------------
% 21.15/3.41 % (1843330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.15/3.41 % (1843330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.41 % (1843330)CaDiCaL version: 2.1.3
% 21.15/3.41 % (1843330)Termination reason: Instruction limit
% 21.15/3.41 % (1843330)Termination phase: Saturation
% 21.15/3.41 % (1843330)Time elapsed: 0.146 s
% 21.15/3.41 % (1843330)Peak memory usage: 12 MB
% 21.15/3.41 % (1843330)Instructions burned: 159 (million)
% 21.15/3.41 % (1843343)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=3841214486:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 21.15/3.41 % (1843349)ott-21_1_sil=16000:fs=off:random_seed=272319592:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 21.15/3.41 % TRYING [7]
% 21.15/3.41 % TRYING [6]
% 21.15/3.41 % (1843339)Instruction limit reached!
% 21.15/3.41 % (1843339)------------------------------
% 21.15/3.41 % (1843339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.20 % (1843339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.20 % (1843339)CaDiCaL version: 2.1.3
% 55.18/8.20 % (1843339)Termination reason: Instruction limit
% 55.18/8.20 % (1843339)Termination phase: Saturation
% 55.18/8.20 % (1843339)Time elapsed: 0.137 s
% 55.18/8.20 % (1843339)Peak memory usage: 12 MB
% 55.18/8.20 % (1843339)Instructions burned: 131 (million)
% 55.18/8.20 % (1843356)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1658493849:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 55.18/8.20 % (1843349)Instruction limit reached!
% 55.18/8.20 % (1843349)------------------------------
% 55.18/8.20 % (1843349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.20 % (1843349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.20 % (1843349)CaDiCaL version: 2.1.3
% 55.18/8.20 % (1843349)Termination reason: Instruction limit
% 55.18/8.20 % (1843349)Termination phase: Saturation
% 55.18/8.20 % (1843349)Time elapsed: 0.155 s
% 55.18/8.20 % (1843349)Peak memory usage: 12 MB
% 55.18/8.20 % (1843349)Instructions burned: 181 (million)
% 55.18/8.20 % (1843358)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1744745713:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 55.18/8.20 % TRYING [1]
% 55.18/8.20 % TRYING [2]
% 55.18/8.20 % TRYING [3]
% 55.18/8.20 % TRYING [4]
% 55.18/8.20 % TRYING [5]
% 55.18/8.20 % TRYING [6]
% 55.18/8.20 % TRYING [8]
% 55.18/8.20 % TRYING [7]
% 55.18/8.20 % TRYING [7]
% 55.18/8.20 % (1843338)Instruction limit reached!
% 55.18/8.20 % (1843338)------------------------------
% 55.18/8.20 % (1843338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.20 % (1843338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.20 % (1843338)CaDiCaL version: 2.1.3
% 55.18/8.20 % (1843338)Termination reason: Instruction limit
% 55.18/8.20 % (1843338)Termination phase: Finite model building constraint generation
% 55.18/8.20 % (1843338)Time elapsed: 0.588 s
% 55.18/8.20 % (1843338)Peak memory usage: 21 MB
% 55.18/8.20 % (1843338)Instructions burned: 715 (million)
% 55.18/8.20 % (1843356)Instruction limit reached!
% 55.18/8.20 % (1843356)------------------------------
% 55.18/8.20 % (1843356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.20 % (1843356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.20 % (1843356)CaDiCaL version: 2.1.3
% 55.18/8.20 % (1843356)Termination reason: Instruction limit
% 55.18/8.20 % (1843356)Termination phase: Saturation
% 55.18/8.20 % (1843356)Time elapsed: 0.409 s
% 55.18/8.20 % (1843356)Peak memory usage: 16 MB
% 55.18/8.20 % (1843356)Instructions burned: 478 (million)
% 55.18/8.20 % (1843364)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4160499737:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 55.18/8.20 % (1843365)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=555589640:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 55.18/8.20 % (1843343)Instruction limit reached!
% 55.18/8.20 % (1843343)------------------------------
% 55.18/8.20 % (1843343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.20 % (1843343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.20 % (1843343)CaDiCaL version: 2.1.3
% 55.18/8.20 % (1843343)Termination reason: Instruction limit
% 55.18/8.20 % (1843343)Termination phase: Saturation
% 55.18/8.20 % (1843343)Time elapsed: 0.614 s
% 55.18/8.20 % (1843343)Peak memory usage: 17 MB
% 55.18/8.20 % (1843343)Instructions burned: 685 (million)
% 55.18/8.20 % (1843369)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=1439380366: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)
% 55.18/8.20 % TRYING [14]
% 55.18/8.20 % (1843358)Instruction limit reached!
% 55.18/8.20 % (1843358)------------------------------
% 55.18/8.20 % (1843358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.20 % (1843358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.20 % (1843358)CaDiCaL version: 2.1.3
% 55.18/8.20 % (1843358)Termination reason: Instruction limit
% 55.18/8.20 % (1843358)Termination phase: Finite model building SAT solving
% 55.18/8.20 % (1843358)Time elapsed: 0.573 s
% 55.18/8.20 % (1843358)Peak memory usage: 21 MB
% 55.18/8.20 % (1843358)Instructions burned: 866 (million)
% 55.18/8.20 % (1843374)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1759692108:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 55.18/8.25 % (1843364)Instruction limit reached!
% 55.18/8.25 % (1843364)------------------------------
% 55.18/8.25 % (1843364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843364)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843364)Termination reason: Instruction limit
% 55.18/8.25 % (1843364)Termination phase: Saturation
% 55.18/8.25 % (1843364)Time elapsed: 0.449 s
% 55.18/8.25 % (1843364)Peak memory usage: 20 MB
% 55.18/8.25 % (1843364)Instructions burned: 1181 (million)
% 55.18/8.25 % (1843380)fmb+10_1_sil=64000:random_seed=3304762437:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 55.18/8.25 % TRYING [1]
% 55.18/8.25 % TRYING [2]
% 55.18/8.25 % TRYING [3]
% 55.18/8.25 % TRYING [4]
% 55.18/8.25 % TRYING [5]
% 55.18/8.25 % TRYING [6]
% 55.18/8.25 % TRYING [7]
% 55.18/8.25 % (1843365)Instruction limit reached!
% 55.18/8.25 % (1843365)------------------------------
% 55.18/8.25 % (1843365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843365)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843365)Termination reason: Instruction limit
% 55.18/8.25 % (1843365)Termination phase: Finite model building constraint generation
% 55.18/8.25 % (1843365)Time elapsed: 0.591 s
% 55.18/8.25 % (1843365)Peak memory usage: 76 MB
% 55.18/8.25 % (1843365)Instructions burned: 889 (million)
% 55.18/8.25 % (1843387)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1950012618:i=9515:nm=5_2986 on theBenchmark for (2986ds/9515Mi)
% 55.18/8.25 % TRYING [20]
% 55.18/8.25 % (1843369)Instruction limit reached!
% 55.18/8.25 % (1843369)------------------------------
% 55.18/8.25 % (1843369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843369)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843369)Termination reason: Instruction limit
% 55.18/8.25 % (1843369)Termination phase: Saturation
% 55.18/8.25 % (1843369)Time elapsed: 0.660 s
% 55.18/8.25 % (1843369)Peak memory usage: 20 MB
% 55.18/8.25 % (1843369)Instructions burned: 692 (million)
% 55.18/8.25 % (1843389)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3956747067:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 55.18/8.25 % TRYING [8]
% 55.18/8.25 % TRYING [8]
% 55.18/8.25 % (1843374)Instruction limit reached!
% 55.18/8.25 % (1843374)------------------------------
% 55.18/8.25 % (1843374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843374)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843374)Termination reason: Instruction limit
% 55.18/8.25 % (1843374)Termination phase: Saturation
% 55.18/8.25 % (1843374)Time elapsed: 0.630 s
% 55.18/8.25 % (1843374)Peak memory usage: 19 MB
% 55.18/8.25 % (1843374)Instructions burned: 880 (million)
% 55.18/8.25 % (1843394)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3915055743:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 55.18/8.25 % TRYING [9]
% 55.18/8.25 % TRYING [9]
% 55.18/8.25 % (1843389)Instruction limit reached!
% 55.18/8.25 % (1843389)------------------------------
% 55.18/8.25 % (1843389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843389)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843389)Termination reason: Instruction limit
% 55.18/8.25 % (1843389)Termination phase: Finite model building SAT solving
% 55.18/8.25 % (1843389)Time elapsed: 0.592 s
% 55.18/8.25 % (1843389)Peak memory usage: 39 MB
% 55.18/8.25 % (1843389)Instructions burned: 921 (million)
% 55.18/8.25 % (1843423)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=996942771:i=1472:ins=7:fdi=8:gsp=on_2978 on theBenchmark for (2978ds/1472Mi)
% 55.18/8.25 % TRYING [10]
% 55.18/8.25 % (1843423)Instruction limit reached!
% 55.18/8.25 % (1843423)------------------------------
% 55.18/8.25 % (1843423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843423)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843423)Termination reason: Instruction limit
% 55.18/8.25 % (1843423)Termination phase: Saturation
% 55.18/8.25 % (1843423)Time elapsed: 0.826 s
% 55.18/8.25 % (1843423)Peak memory usage: 30 MB
% 55.18/8.25 % (1843423)Instructions burned: 1473 (million)
% 55.18/8.25 % (1843551)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3909155715:i=6324_2970 on theBenchmark for (2970ds/6324Mi)
% 55.18/8.25 % TRYING [77]
% 55.18/8.25 % (1843394)Instruction limit reached!
% 55.18/8.25 % (1843394)------------------------------
% 55.18/8.25 % (1843394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843394)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843394)Termination reason: Instruction limit
% 55.18/8.25 % (1843394)Termination phase: Saturation
% 55.18/8.25 % (1843394)Time elapsed: 2.881 s
% 55.18/8.25 % (1843394)Peak memory usage: 49 MB
% 55.18/8.25 % (1843394)Instructions burned: 5131 (million)
% 55.18/8.25 % (1843553)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3270072435:fmbsr=2.30978:i=2174_2954 on theBenchmark for (2954ds/2174Mi)
% 55.18/8.25 % TRYING [16]
% 55.18/8.25 % TRYING [10]
% 55.18/8.25 % (1843387)Instruction limit reached!
% 55.18/8.25 % (1843387)------------------------------
% 55.18/8.25 % (1843387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843387)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843387)Termination reason: Instruction limit
% 55.18/8.25 % (1843387)Termination phase: Finite model building constraint generation
% 55.18/8.25 % (1843387)Time elapsed: 3.709 s
% 55.18/8.25 % (1843387)Peak memory usage: 705 MB
% 55.18/8.25 % (1843387)Instructions burned: 9516 (million)
% 55.18/8.25 % (1843555)ott-2_1_sil=16000:newcnf=on:random_seed=2107340897:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2947 on theBenchmark for (2947ds/869Mi)
% 55.18/8.25 % (1843553)Instruction limit reached!
% 55.18/8.25 % (1843553)------------------------------
% 55.18/8.25 % (1843553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843553)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843553)Termination reason: Instruction limit
% 55.18/8.25 % (1843553)Termination phase: Finite model building constraint generation
% 55.18/8.25 % (1843553)Time elapsed: 0.736 s
% 55.18/8.25 % (1843553)Peak memory usage: 135 MB
% 55.18/8.25 % (1843553)Instructions burned: 2176 (million)
% 55.18/8.25 % (1843551)Instruction limit reached!
% 55.18/8.25 % (1843551)------------------------------
% 55.18/8.25 % (1843551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843551)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843551)Termination reason: Instruction limit
% 55.18/8.25 % (1843551)Termination phase: Finite model building constraint generation
% 55.18/8.25 % (1843551)Time elapsed: 2.332 s
% 55.18/8.25 % (1843551)Peak memory usage: 436 MB
% 55.18/8.25 % (1843551)Instructions burned: 6324 (million)
% 55.18/8.25 % TRYING [11]
% 55.18/8.25 % (1843557)ott+10_1_sil=32000:tgt=ground:random_seed=1791491429:i=5114:av=off_2946 on theBenchmark for (2946ds/5114Mi)
% 55.18/8.25 % (1843559)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2880082080:i=54282_2946 on theBenchmark for (2946ds/54282Mi)
% 55.18/8.25 % TRYING [1]
% 55.18/8.25 % TRYING [2]
% 55.18/8.25 % TRYING [3]
% 55.18/8.25 % TRYING [4]
% 55.18/8.25 % TRYING [5]
% 55.18/8.25 % TRYING [6]
% 55.18/8.25 % TRYING [7]
% 55.18/8.25 % TRYING [8]
% 55.18/8.25 % (1843555)Instruction limit reached!
% 55.18/8.25 % (1843555)------------------------------
% 55.18/8.25 % (1843555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843555)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843555)Termination reason: Instruction limit
% 55.18/8.25 % (1843555)Termination phase: Saturation
% 55.18/8.25 % (1843555)Time elapsed: 0.533 s
% 55.18/8.25 % (1843555)Peak memory usage: 20 MB
% 55.18/8.25 % (1843555)Instructions burned: 869 (million)
% 55.18/8.25 % (1843561)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=423190803:i=3512:aac=none_2942 on theBenchmark for (2942ds/3512Mi)
% 55.18/8.25 % TRYING [9]
% 55.18/8.25 % (1843561)Instruction limit reached!
% 55.18/8.25 % (1843561)------------------------------
% 55.18/8.25 % (1843561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.25 % (1843561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.25 % (1843561)CaDiCaL version: 2.1.3
% 55.18/8.25 % (1843561)Termination reason: Instruction limit
% 55.18/8.25 % (1843561)Termination phase: Saturation
% 55.18/8.25 % (1843561)Time elapsed: 2.002 s
% 55.18/8.25 % (1843561)Peak memory usage: 43 MB
% 55.18/8.25 % (1843561)Instructions burned: 3513 (million)
% 55.18/8.25 % (1843557) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1843319-1843557"...
% 55.18/8.25 % (1843563)dis+21_1_sil=32000:sas=cadical:random_seed=1927111788:i=3773:amm=off_2922 on theBenchmark for (2922ds/3773Mi)
% 55.18/8.25 % (1843557)...printing done.
% 55.18/8.25 % (1843557)Refutation found. Thanks to Tanya!
% 55.18/8.25 % SZS status Unsatisfiable for theBenchmark
% 55.18/8.25 % SZS output start Proof for theBenchmark
% See solution above
% 55.18/8.26 % (1843557)------------------------------
% 55.18/8.26 % (1843557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.18/8.26 % (1843557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.18/8.26 % (1843557)CaDiCaL version: 2.1.3
% 55.18/8.26 % (1843557)Termination reason: Refutation
% 55.18/8.26 % (1843557)Time elapsed: 2.468 s
% 55.18/8.26 % (1843557)Peak memory usage: 54 MB
% 55.18/8.26 % (1843557)Instructions burned: 3947 (million)
% 55.18/8.26 % (1843319)Success in time 7.835 s
% 55.18/8.26 % Vampire exiting
%------------------------------------------------------------------------------