%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX185+1 : TPTP v9.3.1. Released v9.3.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 01:46:39 PM UTC 2026
% Result : Theorem 44.07s 12.72s
% Output : Refutation 44.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 10
% Syntax : Number of formulae : 47 ( 30 unt; 0 def)
% Number of atoms : 68 ( 67 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 41 ( 20 ~; 17 |; 0 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-2 aty)
% Number of variables : 72 ( 68 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,axiom,
! [X0,X1] : proj22(x2(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_022) ).
fof(f24,axiom,
! [X0,X1] : z(X0,X1) != eX,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_024) ).
fof(f26,axiom,
! [X0,X1] : x2(X0,X1) != eX,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_026) ).
fof(f29,axiom,
! [X0] :
( X0 != z(proj1(X0),proj2(X0))
=> ( X0 != x2(proj12(X0),proj22(X0))
=> assoc(X0) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_029) ).
fof(f32,axiom,
! [X0,X1] : assoc(x2(X0,X1)) = x2(assoc(X0),assoc(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_032) ).
fof(f33,axiom,
! [X0] : append(nil,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_033) ).
fof(f34,axiom,
! [X0,X1,X2] : append(cons(X1,X2),X0) = cons(X1,append(X2,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_034) ).
fof(f38,axiom,
! [X0,X1] : lin(x2(X0,X1)) = append(lin(X0),append(cons(mul,nil),lin(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_038) ).
fof(f39,axiom,
lin(eX) = cons(x,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_039) ).
fof(f41,conjecture,
? [X0,X1] :
~ ( lin(X0) = lin(X1)
=> assoc(X0) = assoc(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_041) ).
fof(f42,negated_conjecture,
~ ? [X0,X1] :
~ ( lin(X0) = lin(X1)
=> assoc(X0) = assoc(X1) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f43,plain,
! [X0] :
( assoc(X0) = X0
| x2(proj12(X0),proj22(X0)) = X0
| z(proj1(X0),proj2(X0)) = X0 ),
inference(ennf_transformation,[],[f29]) ).
fof(f44,plain,
! [X0] :
( assoc(X0) = X0
| x2(proj12(X0),proj22(X0)) = X0
| z(proj1(X0),proj2(X0)) = X0 ),
inference(flattening,[],[f43]) ).
fof(f47,plain,
! [X0,X1] :
( assoc(X0) = assoc(X1)
| lin(X0) != lin(X1) ),
inference(ennf_transformation,[],[f42]) ).
fof(f69,plain,
! [X0,X1] : proj22(x2(X0,X1)) = X1,
inference(cnf_transformation,[],[f22]) ).
fof(f71,plain,
! [X0,X1] : z(X0,X1) != eX,
inference(cnf_transformation,[],[f24]) ).
fof(f73,plain,
! [X0,X1] : x2(X0,X1) != eX,
inference(cnf_transformation,[],[f26]) ).
fof(f76,plain,
! [X0] :
( x2(proj12(X0),proj22(X0)) = X0
| assoc(X0) = X0
| z(proj1(X0),proj2(X0)) = X0 ),
inference(cnf_transformation,[],[f44]) ).
fof(f79,plain,
! [X0,X1] : assoc(x2(X0,X1)) = x2(assoc(X0),assoc(X1)),
inference(cnf_transformation,[],[f32]) ).
fof(f80,plain,
! [X0] : append(nil,X0) = X0,
inference(cnf_transformation,[],[f33]) ).
fof(f81,plain,
! [X2,X0,X1] : append(cons(X1,X2),X0) = cons(X1,append(X2,X0)),
inference(cnf_transformation,[],[f34]) ).
fof(f85,plain,
! [X0,X1] : lin(x2(X0,X1)) = append(lin(X0),append(cons(mul,nil),lin(X1))),
inference(cnf_transformation,[],[f38]) ).
fof(f86,plain,
lin(eX) = cons(x,nil),
inference(cnf_transformation,[],[f39]) ).
fof(f88,plain,
! [X0,X1] :
( lin(X0) != lin(X1)
| assoc(X0) = assoc(X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f236,plain,
! [X0,X1] : lin(x2(X0,X1)) = append(lin(X0),cons(mul,append(nil,lin(X1)))),
inference(forward_demodulation,[],[f85,f81]) ).
fof(f237,plain,
! [X0,X1] : lin(x2(X0,X1)) = append(lin(X0),cons(mul,lin(X1))),
inference(forward_demodulation,[],[f236,f80]) ).
fof(f238,plain,
! [X0] : lin(x2(eX,X0)) = append(cons(x,nil),cons(mul,lin(X0))),
inference(superposition,[],[f237,f86]) ).
fof(f241,plain,
! [X0] : lin(x2(X0,eX)) = append(lin(X0),cons(mul,cons(x,nil))),
inference(superposition,[],[f237,f86]) ).
fof(f246,plain,
! [X0] : lin(x2(eX,X0)) = cons(x,append(nil,cons(mul,lin(X0)))),
inference(forward_demodulation,[],[f238,f81]) ).
fof(f249,plain,
! [X0] : lin(x2(eX,X0)) = cons(x,cons(mul,lin(X0))),
inference(forward_demodulation,[],[f246,f80]) ).
fof(f1096,plain,
eX = assoc(eX),
inference(unit_resulting_resolution,[],[f76,f71,f73]) ).
fof(f2809,plain,
! [X0,X1] :
( lin(X1) != append(lin(X0),cons(mul,cons(x,nil)))
| assoc(X1) = assoc(x2(X0,eX)) ),
inference(superposition,[],[f88,f241]) ).
fof(f3117,plain,
! [X0,X1] :
( assoc(X1) = x2(assoc(X0),assoc(eX))
| lin(X1) != append(lin(X0),cons(mul,cons(x,nil))) ),
inference(forward_demodulation,[],[f2809,f79]) ).
fof(f3255,plain,
! [X0,X1] :
( lin(X1) != append(lin(X0),cons(mul,cons(x,nil)))
| assoc(X1) = x2(assoc(X0),eX) ),
inference(forward_demodulation,[],[f3117,f1096]) ).
fof(f3546,plain,
! [X0,X1] :
( lin(X1) != append(cons(x,cons(mul,lin(X0))),cons(mul,cons(x,nil)))
| assoc(X1) = x2(assoc(x2(eX,X0)),eX) ),
inference(superposition,[],[f3255,f249]) ).
fof(f3554,plain,
! [X0,X1] :
( lin(X1) != cons(x,append(cons(mul,lin(X0)),cons(mul,cons(x,nil))))
| assoc(X1) = x2(assoc(x2(eX,X0)),eX) ),
inference(forward_demodulation,[],[f3546,f81]) ).
fof(f3564,plain,
! [X0,X1] :
( lin(X1) != cons(x,cons(mul,append(lin(X0),cons(mul,cons(x,nil)))))
| assoc(X1) = x2(assoc(x2(eX,X0)),eX) ),
inference(forward_demodulation,[],[f3554,f81]) ).
fof(f3572,plain,
! [X0,X1] :
( assoc(X1) = x2(x2(assoc(eX),assoc(X0)),eX)
| lin(X1) != cons(x,cons(mul,append(lin(X0),cons(mul,cons(x,nil))))) ),
inference(forward_demodulation,[],[f3564,f79]) ).
fof(f3575,plain,
! [X0,X1] :
( lin(X1) != cons(x,cons(mul,append(lin(X0),cons(mul,cons(x,nil)))))
| assoc(X1) = x2(x2(eX,assoc(X0)),eX) ),
inference(forward_demodulation,[],[f3572,f1096]) ).
fof(f7367,plain,
! [X0,X1] :
( lin(X1) != cons(x,cons(mul,lin(x2(X0,eX))))
| assoc(X1) = x2(x2(eX,assoc(X0)),eX) ),
inference(superposition,[],[f3575,f241]) ).
fof(f7400,plain,
! [X0] : x2(x2(eX,assoc(X0)),eX) = assoc(x2(eX,x2(X0,eX))),
inference(unit_resulting_resolution,[],[f7367,f249]) ).
fof(f7416,plain,
! [X0] : x2(x2(eX,assoc(X0)),eX) = x2(assoc(eX),assoc(x2(X0,eX))),
inference(forward_demodulation,[],[f7400,f79]) ).
fof(f7423,plain,
! [X0] : x2(x2(eX,assoc(X0)),eX) = x2(assoc(eX),x2(assoc(X0),assoc(eX))),
inference(forward_demodulation,[],[f7416,f79]) ).
fof(f7424,plain,
! [X0] : x2(eX,x2(assoc(X0),eX)) = x2(x2(eX,assoc(X0)),eX),
inference(forward_demodulation,[],[f7423,f1096]) ).
fof(f7458,plain,
! [X0] : eX = proj22(x2(eX,x2(assoc(X0),eX))),
inference(superposition,[],[f69,f7424]) ).
fof(f7467,plain,
! [X0] : eX = x2(assoc(X0),eX),
inference(forward_demodulation,[],[f7458,f69]) ).
fof(f7495,plain,
$false,
inference(forward_subsumption_resolution,[],[f7467,f73]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX185+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n003.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 15:08:27 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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.03/3.21 % (1687614)Will run a generic schedule for satisfiability detection.
% 21.03/3.21 % (1687620)% WARNING: option uhcvi not known.
% 21.03/3.21 % (1687620)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3562414401:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 21.03/3.21 % (1687619)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1295342458_2999 on theBenchmark for (2999ds/0Mi)
% 21.03/3.21 % (1687621)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2165233297:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 21.03/3.21 % (1687622)dis+10_1_sil=32000:sp=arity:random_seed=2884235429:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 21.03/3.21 % (1687623)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3815246649:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 21.03/3.21 % Detected minimum model sizes of [6]
% 21.03/3.21 % Detected maximum model sizes of [max]
% 21.03/3.21 % TRYING [6]
% 21.03/3.21 % (1687625)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3805765585:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 21.03/3.21 % (1687624)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1371624578:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 21.03/3.21 % (1687622)Instruction limit reached!
% 21.03/3.21 % (1687622)------------------------------
% 21.03/3.21 % (1687622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.03/3.21 % (1687622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.03/3.21 % (1687622)CaDiCaL version: 2.1.3
% 21.03/3.21 % (1687622)Termination reason: Instruction limit
% 21.03/3.21 % (1687622)Termination phase: Saturation
% 21.03/3.21 % (1687622)Time elapsed: 0.057 s
% 21.03/3.21 % (1687622)Peak memory usage: 12 MB
% 21.03/3.21 % (1687622)Instructions burned: 104 (million)
% 21.03/3.21 % (1687623)Instruction limit reached!
% 21.03/3.21 % (1687623)------------------------------
% 21.03/3.21 % (1687623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.03/3.21 % (1687623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.03/3.21 % (1687623)CaDiCaL version: 2.1.3
% 21.03/3.21 % (1687623)Termination reason: Instruction limit
% 21.03/3.21 % (1687623)Termination phase: Saturation
% 21.03/3.21 % (1687623)Time elapsed: 0.063 s
% 21.03/3.21 % (1687623)Peak memory usage: 12 MB
% 21.03/3.21 % (1687623)Instructions burned: 118 (million)
% 21.03/3.21 % TRYING [7]
% 21.03/3.21 % (1687633)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4224809195:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 21.03/3.21 % Detected minimum model sizes of [6]
% 21.03/3.21 % Detected maximum model sizes of [max]
% 21.03/3.21 % TRYING [6]
% 21.03/3.21 % (1687634)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2026075723:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 21.03/3.21 % (1687624)Instruction limit reached!
% 21.03/3.21 % (1687624)------------------------------
% 21.03/3.21 % (1687624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.03/3.21 % (1687624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.03/3.21 % (1687624)CaDiCaL version: 2.1.3
% 21.03/3.21 % (1687624)Termination reason: Instruction limit
% 21.03/3.21 % (1687624)Termination phase: Saturation
% 21.03/3.21 % (1687624)Time elapsed: 0.069 s
% 21.03/3.21 % (1687624)Peak memory usage: 13 MB
% 21.03/3.21 % (1687624)Instructions burned: 131 (million)
% 21.03/3.21 % (1687637)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=2916624320:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 21.03/3.21 % (1687625)Instruction limit reached!
% 21.03/3.21 % (1687625)------------------------------
% 21.03/3.21 % (1687625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.03/3.21 % (1687625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.03/3.21 % (1687625)CaDiCaL version: 2.1.3
% 21.03/3.21 % (1687625)Termination reason: Instruction limit
% 21.03/3.21 % (1687625)Termination phase: Saturation
% 21.03/3.21 % (1687625)Time elapsed: 0.111 s
% 21.03/3.21 % (1687625)Peak memory usage: 13 MB
% 21.03/3.21 % (1687625)Instructions burned: 159 (million)
% 21.03/3.21 % (1687639)ott-21_1_sil=16000:fs=off:random_seed=2536561602:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 21.03/3.21 % (1687634)Instruction limit reached!
% 21.03/3.21 % (1687634)------------------------------
% 21.03/3.21 % (1687634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.72/8.46 % (1687634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.72/8.46 % (1687634)CaDiCaL version: 2.1.3
% 57.72/8.46 % (1687634)Termination reason: Instruction limit
% 57.72/8.46 % (1687634)Termination phase: Saturation
% 57.72/8.46 % (1687634)Time elapsed: 0.086 s
% 57.72/8.46 % (1687634)Peak memory usage: 12 MB
% 57.72/8.46 % (1687634)Instructions burned: 139 (million)
% 57.72/8.46 % (1687641)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1507971690:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 57.72/8.46 % TRYING [8]
% 57.72/8.46 % TRYING [7]
% 57.72/8.46 % (1687639)Instruction limit reached!
% 57.72/8.46 % (1687639)------------------------------
% 57.72/8.46 % (1687639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.72/8.46 % (1687639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.72/8.46 % (1687639)CaDiCaL version: 2.1.3
% 57.72/8.46 % (1687639)Termination reason: Instruction limit
% 57.72/8.46 % (1687639)Termination phase: Saturation
% 57.72/8.46 % (1687639)Time elapsed: 0.095 s
% 57.72/8.46 % (1687639)Peak memory usage: 12 MB
% 57.72/8.46 % (1687639)Instructions burned: 181 (million)
% 57.72/8.46 % (1687660)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1077182607:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 57.72/8.46 % Detected minimum model sizes of [6]
% 57.72/8.46 % Detected maximum model sizes of [max]
% 57.72/8.46 % TRYING [6]
% 57.72/8.46 % (1687637)Instruction limit reached!
% 57.72/8.46 % (1687637)------------------------------
% 57.72/8.46 % (1687637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.72/8.46 % (1687637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.72/8.46 % (1687637)CaDiCaL version: 2.1.3
% 57.72/8.46 % (1687637)Termination reason: Instruction limit
% 57.72/8.46 % (1687637)Termination phase: Saturation
% 57.72/8.46 % (1687637)Time elapsed: 0.197 s
% 57.72/8.46 % (1687637)Peak memory usage: 17 MB
% 57.72/8.46 % (1687637)Instructions burned: 684 (million)
% 57.72/8.46 % (1687691)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3406698130:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 57.72/8.46 % (1687633)Instruction limit reached!
% 57.72/8.46 % (1687633)------------------------------
% 57.72/8.46 % (1687633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.72/8.46 % (1687633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.72/8.46 % (1687633)CaDiCaL version: 2.1.3
% 57.72/8.46 % (1687633)Termination reason: Instruction limit
% 57.72/8.46 % (1687633)Termination phase: Finite model building SAT solving
% 57.72/8.46 % (1687633)Time elapsed: 0.289 s
% 57.72/8.46 % (1687633)Peak memory usage: 35 MB
% 57.72/8.46 % (1687633)Instructions burned: 715 (million)
% 57.72/8.46 % (1687713)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1431039892:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 57.72/8.46 % TRYING [9]
% 57.72/8.46 % TRYING [7]
% 57.72/8.46 % TRYING [14]
% 57.72/8.46 % (1687641)Instruction limit reached!
% 57.72/8.46 % (1687641)------------------------------
% 57.72/8.46 % (1687641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.72/8.46 % (1687641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.72/8.46 % (1687641)CaDiCaL version: 2.1.3
% 57.72/8.46 % (1687641)Termination reason: Instruction limit
% 57.72/8.46 % (1687641)Termination phase: Saturation
% 57.72/8.46 % (1687641)Time elapsed: 0.284 s
% 57.72/8.46 % (1687641)Peak memory usage: 14 MB
% 57.72/8.46 % (1687641)Instructions burned: 477 (million)
% 57.72/8.46 % (1687745)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=1070625094:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 57.72/8.46 % (1687660)Instruction limit reached!
% 57.72/8.46 % (1687660)------------------------------
% 57.72/8.46 % (1687660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.72/8.46 % (1687660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.72/8.46 % (1687660)CaDiCaL version: 2.1.3
% 57.72/8.46 % (1687660)Termination reason: Instruction limit
% 57.72/8.46 % (1687660)Termination phase: Finite model building SAT solving
% 57.72/8.46 % (1687660)Time elapsed: 0.329 s
% 57.72/8.46 % (1687660)Peak memory usage: 27 MB
% 57.72/8.46 % (1687660)Instructions burned: 867 (million)
% 57.72/8.46 % (1687772)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2906681371:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 44.07/12.72 % (1687691)Instruction limit reached!
% 44.07/12.72 % (1687691)------------------------------
% 44.07/12.72 % (1687691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687691)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687691)Termination reason: Instruction limit
% 44.07/12.72 % (1687691)Termination phase: Saturation
% 44.07/12.72 % (1687691)Time elapsed: 0.380 s
% 44.07/12.72 % (1687691)Peak memory usage: 20 MB
% 44.07/12.72 % (1687691)Instructions burned: 1181 (million)
% 44.07/12.72 % (1687797)fmb+10_1_sil=64000:random_seed=3370130161:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 44.07/12.72 % Detected minimum model sizes of [6]
% 44.07/12.72 % Detected maximum model sizes of [max]
% 44.07/12.72 % TRYING [6]
% 44.07/12.72 % (1687713)Instruction limit reached!
% 44.07/12.72 % (1687713)------------------------------
% 44.07/12.72 % (1687713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687713)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687713)Termination reason: Instruction limit
% 44.07/12.72 % (1687713)Termination phase: Finite model building constraint generation
% 44.07/12.72 % (1687713)Time elapsed: 0.428 s
% 44.07/12.72 % (1687713)Peak memory usage: 77 MB
% 44.07/12.72 % (1687713)Instructions burned: 890 (million)
% 44.07/12.72 % TRYING [7]
% 44.07/12.72 % (1687807)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3468256836:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 44.07/12.72 % Detected minimum model sizes of [6]
% 44.07/12.72 % Detected maximum model sizes of [max]
% 44.07/12.72 % TRYING [20]
% 44.07/12.72 % TRYING [10]
% 44.07/12.72 % (1687745)Instruction limit reached!
% 44.07/12.72 % (1687745)------------------------------
% 44.07/12.72 % (1687745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687745)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687745)Termination reason: Instruction limit
% 44.07/12.72 % (1687745)Termination phase: Saturation
% 44.07/12.72 % (1687745)Time elapsed: 0.573 s
% 44.07/12.72 % (1687745)Peak memory usage: 20 MB
% 44.07/12.72 % (1687745)Instructions burned: 693 (million)
% 44.07/12.72 % TRYING [8]
% 44.07/12.72 % (1687813)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=185438870:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 44.07/12.72 % Detected minimum model sizes of [6]
% 44.07/12.72 % Detected maximum model sizes of [max]
% 44.07/12.72 % TRYING [8]
% 44.07/12.72 % (1687772)Instruction limit reached!
% 44.07/12.72 % (1687772)------------------------------
% 44.07/12.72 % (1687772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687772)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687772)Termination reason: Instruction limit
% 44.07/12.72 % (1687772)Termination phase: Saturation
% 44.07/12.72 % (1687772)Time elapsed: 0.817 s
% 44.07/12.72 % (1687772)Peak memory usage: 18 MB
% 44.07/12.72 % (1687772)Instructions burned: 880 (million)
% 44.07/12.72 % (1687820)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3343260057:i=5131_2985 on theBenchmark for (2985ds/5131Mi)
% 44.07/12.72 % TRYING [9]
% 44.07/12.72 % (1687813)Instruction limit reached!
% 44.07/12.72 % (1687813)------------------------------
% 44.07/12.72 % (1687813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687813)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687813)Termination reason: Instruction limit
% 44.07/12.72 % (1687813)Termination phase: Finite model building constraint generation
% 44.07/12.72 % (1687813)Time elapsed: 0.654 s
% 44.07/12.72 % (1687813)Peak memory usage: 47 MB
% 44.07/12.72 % (1687813)Instructions burned: 920 (million)
% 44.07/12.72 % (1687827)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=808405286:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 44.07/12.72 % TRYING [9]
% 44.07/12.72 % TRYING [11]
% 44.07/12.72 % TRYING [10]
% 44.07/12.72 % (1687827)Instruction limit reached!
% 44.07/12.72 % (1687827)------------------------------
% 44.07/12.72 % (1687827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687827)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687827)Termination reason: Instruction limit
% 44.07/12.72 % (1687827)Termination phase: Saturation
% 44.07/12.72 % (1687827)Time elapsed: 1.143 s
% 44.07/12.72 % (1687827)Peak memory usage: 19 MB
% 44.07/12.72 % (1687827)Instructions burned: 1472 (million)
% 44.07/12.72 % (1687837)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1509683861:i=6324_2970 on theBenchmark for (2970ds/6324Mi)
% 44.07/12.72 % Detected minimum model sizes of [6]
% 44.07/12.72 % Detected maximum model sizes of [max]
% 44.07/12.72 % TRYING [77]
% 44.07/12.72 % TRYING [12]
% 44.07/12.72 % TRYING [11]
% 44.07/12.72 % (1687820)Instruction limit reached!
% 44.07/12.72 % (1687820)------------------------------
% 44.07/12.72 % (1687820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687820)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687820)Termination reason: Instruction limit
% 44.07/12.72 % (1687820)Termination phase: Saturation
% 44.07/12.72 % (1687820)Time elapsed: 4.343 s
% 44.07/12.72 % (1687820)Peak memory usage: 24 MB
% 44.07/12.72 % (1687820)Instructions burned: 5131 (million)
% 44.07/12.72 % (1687843)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=510238183:fmbsr=2.30978:i=2174_2941 on theBenchmark for (2941ds/2174Mi)
% 44.07/12.72 % Detected minimum model sizes of [6]
% 44.07/12.72 % Detected maximum model sizes of [max]
% 44.07/12.72 % TRYING [16]
% 44.07/12.72 % TRYING [12]
% 44.07/12.72 % (1687843)Instruction limit reached!
% 44.07/12.72 % (1687843)------------------------------
% 44.07/12.72 % (1687843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687843)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687843)Termination reason: Instruction limit
% 44.07/12.72 % (1687843)Termination phase: Finite model building constraint generation
% 44.07/12.72 % (1687843)Time elapsed: 1.461 s
% 44.07/12.72 % (1687843)Peak memory usage: 134 MB
% 44.07/12.72 % (1687843)Instructions burned: 2175 (million)
% 44.07/12.72 % (1687851)ott-2_1_sil=16000:newcnf=on:random_seed=1092568362:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2926 on theBenchmark for (2926ds/869Mi)
% 44.07/12.72 % TRYING [13]
% 44.07/12.72 % (1687837)Instruction limit reached!
% 44.07/12.72 % (1687837)------------------------------
% 44.07/12.72 % (1687837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687837)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687837)Termination reason: Instruction limit
% 44.07/12.72 % (1687837)Termination phase: Finite model building constraint generation
% 44.07/12.72 % (1687837)Time elapsed: 4.426 s
% 44.07/12.72 % (1687837)Peak memory usage: 509 MB
% 44.07/12.72 % (1687837)Instructions burned: 6325 (million)
% 44.07/12.72 % (1687853)ott+10_1_sil=32000:tgt=ground:random_seed=3657539407:i=5114:av=off_2924 on theBenchmark for (2924ds/5114Mi)
% 44.07/12.72 % (1687807)Instruction limit reached!
% 44.07/12.72 % (1687807)------------------------------
% 44.07/12.72 % (1687807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687807)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687807)Termination reason: Instruction limit
% 44.07/12.72 % (1687807)Termination phase: Finite model building constraint generation
% 44.07/12.72 % (1687807)Time elapsed: 6.876 s
% 44.07/12.72 % (1687807)Peak memory usage: 676 MB
% 44.07/12.72 % (1687807)Instructions burned: 9516 (million)
% 44.07/12.72 % (1687855)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=146670468:i=54282_2920 on theBenchmark for (2920ds/54282Mi)
% 44.07/12.72 % Detected minimum model sizes of [6]
% 44.07/12.72 % Detected maximum model sizes of [max]
% 44.07/12.72 % TRYING [6]
% 44.07/12.72 % TRYING [7]
% 44.07/12.72 % (1687851)Instruction limit reached!
% 44.07/12.72 % (1687851)------------------------------
% 44.07/12.72 % (1687851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687851)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687851)Termination reason: Instruction limit
% 44.07/12.72 % (1687851)Termination phase: Saturation
% 44.07/12.72 % (1687851)Time elapsed: 0.816 s
% 44.07/12.72 % (1687851)Peak memory usage: 18 MB
% 44.07/12.72 % (1687851)Instructions burned: 870 (million)
% 44.07/12.72 % (1687857)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2203179186:i=3512:aac=none_2917 on theBenchmark for (2917ds/3512Mi)
% 44.07/12.72 % TRYING [8]
% 44.07/12.72 % TRYING [9]
% 44.07/12.72 % (1687797)Instruction limit reached!
% 44.07/12.72 % (1687797)------------------------------
% 44.07/12.72 % (1687797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687797)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687797)Termination reason: Instruction limit
% 44.07/12.72 % (1687797)Termination phase: Finite model building SAT solving
% 44.07/12.72 % (1687797)Time elapsed: 8.233 s
% 44.07/12.72 % (1687797)Peak memory usage: 223 MB
% 44.07/12.72 % (1687797)Instructions burned: 22063 (million)
% 44.07/12.72 % (1687861)dis+21_1_sil=32000:sas=cadical:random_seed=166311787:i=3773:amm=off_2909 on theBenchmark for (2909ds/3773Mi)
% 44.07/12.72 % TRYING [10]
% 44.07/12.72 % TRYING [11]
% 44.07/12.72 % (1687861)Instruction limit reached!
% 44.07/12.72 % (1687861)------------------------------
% 44.07/12.72 % (1687861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687861)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687861)Termination reason: Instruction limit
% 44.07/12.72 % (1687861)Termination phase: Saturation
% 44.07/12.72 % (1687861)Time elapsed: 1.678 s
% 44.07/12.72 % (1687861)Peak memory usage: 23 MB
% 44.07/12.72 % (1687861)Instructions burned: 3775 (million)
% 44.07/12.72 % (1687863)ott+11_1_sil=16000:gs=on:random_seed=2871309704:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2892 on theBenchmark for (2892ds/2251Mi)
% 44.07/12.72 % (1687857)Instruction limit reached!
% 44.07/12.72 % (1687857)------------------------------
% 44.07/12.72 % (1687857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687857)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687857)Termination reason: Instruction limit
% 44.07/12.72 % (1687857)Termination phase: Saturation
% 44.07/12.72 % (1687857)Time elapsed: 3.057 s
% 44.07/12.72 % (1687857)Peak memory usage: 22 MB
% 44.07/12.72 % (1687857)Instructions burned: 3512 (million)
% 44.07/12.72 % (1687867)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3515590776:fmbsr=1.6:i=67534_2886 on theBenchmark for (2886ds/67534Mi)
% 44.07/12.72 % Detected minimum model sizes of [6]
% 44.07/12.72 % Detected maximum model sizes of [max]
% 44.07/12.72 % TRYING [7]
% 44.07/12.72 % TRYING [14]
% 44.07/12.72 % (1687863)Instruction limit reached!
% 44.07/12.72 % (1687863)------------------------------
% 44.07/12.72 % (1687863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687863)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687863)Termination reason: Instruction limit
% 44.07/12.72 % (1687863)Termination phase: Saturation
% 44.07/12.72 % (1687863)Time elapsed: 0.967 s
% 44.07/12.72 % (1687863)Peak memory usage: 15 MB
% 44.07/12.72 % (1687863)Instructions burned: 2252 (million)
% 44.07/12.72 % (1687869)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1008070656:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2882 on theBenchmark for (2882ds/4591Mi)
% 44.07/12.72 % (1687853)Instruction limit reached!
% 44.07/12.72 % (1687853)------------------------------
% 44.07/12.72 % (1687853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687853)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687853)Termination reason: Instruction limit
% 44.07/12.72 % (1687853)Termination phase: Saturation
% 44.07/12.72 % (1687853)Time elapsed: 4.295 s
% 44.07/12.72 % (1687853)Peak memory usage: 30 MB
% 44.07/12.72 % (1687853)Instructions burned: 5114 (million)
% 44.07/12.72 % (1687871)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2085028425:i=29340_2881 on theBenchmark for (2881ds/29340Mi)
% 44.07/12.72 % TRYING [8]
% 44.07/12.72 % (1687871) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1687614-1687871"...
% 44.07/12.72 % (1687871)...printing done.
% 44.07/12.72 % (1687871)Refutation found. Thanks to Tanya!
% 44.07/12.72 % SZS status Theorem for theBenchmark
% 44.07/12.72 % SZS output start Proof for theBenchmark
% See solution above
% 44.07/12.72 % (1687871)------------------------------
% 44.07/12.72 % (1687871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.07/12.72 % (1687871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.07/12.72 % (1687871)CaDiCaL version: 2.1.3
% 44.07/12.72 % (1687871)Termination reason: Refutation
% 44.07/12.72 % (1687871)Time elapsed: 0.507 s
% 44.07/12.72 % (1687871)Peak memory usage: 15 MB
% 44.07/12.72 % (1687871)Instructions burned: 570 (million)
% 44.07/12.72 % (1687614)Success in time 12.498 s
% 44.07/12.72 % Vampire exiting
%------------------------------------------------------------------------------