%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX240-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 : n010.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:49 PM UTC 2026
% Result : Unsatisfiable 21.16s 3.37s
% Output : Refutation 21.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 26
% Syntax : Number of formulae : 67 ( 67 unt; 0 def)
% Number of atoms : 67 ( 66 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 16 ( 16 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 8 con; 0-5 aty)
% Number of variables : 106 ( 106 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X2,X0,X1] : aux2(X0,X1,X2,btrue) = cons(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_002) ).
fof(f5,axiom,
! [X2,X3,X0,X1] : aux3(X0,X1,X2,X3,btrue) = run(X0,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_004) ).
fof(f6,axiom,
! [X2,X3,X0,X1] : aux3(X0,X1,X2,X3,bfalse) = run(X0,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
fof(f7,axiom,
! [X0] : orb(btrue,X0) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
fof(f8,plain,
! [X0] : btrue = orb(btrue,X0),
inference(reorient_equations,[],[f7]) ).
fof(f15,axiom,
secret(tT) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_011) ).
fof(f16,plain,
bfalse = secret(tT),
inference(reorient_equations,[],[f15]) ).
fof(f21,axiom,
notb(bfalse) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_014) ).
fof(f22,plain,
btrue = notb(bfalse),
inference(reorient_equations,[],[f21]) ).
fof(f23,axiom,
l = low(zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_015) ).
fof(f24,axiom,
! [X0] : impl(btrue,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
fof(f28,axiom,
! [X0] : elem(X0,nil) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_019) ).
fof(f29,plain,
! [X0] : bfalse = elem(X0,nil),
inference(reorient_equations,[],[f28]) ).
fof(f30,axiom,
! [X2,X0,X1] : elem(X0,cons(X1,X2)) = orb(eq2(X1,X0),elem(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_020) ).
fof(f34,axiom,
! [X0] : andb(btrue,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_023) ).
fof(f38,axiom,
! [X0] : eval(X0,tT) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_026) ).
fof(f39,plain,
! [X0] : btrue = eval(X0,tT),
inference(reorient_equations,[],[f38]) ).
fof(f42,axiom,
! [X0,X1] : eval(X0,var(X1)) = elem(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_028) ).
fof(f43,axiom,
! [X0] : run(X0,skip) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_029) ).
fof(f44,axiom,
! [X2,X0,X1] : run(X0,assign(X1,X2)) = aux2(X0,X1,X2,eval(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_030) ).
fof(f46,axiom,
! [X2,X3,X0,X1] : run(X0,ifThenElse(X1,X2,X3)) = aux3(X0,X1,X2,X3,eval(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_032) ).
fof(f47,axiom,
typeCorrect(skip) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_033) ).
fof(f48,plain,
btrue = typeCorrect(skip),
inference(reorient_equations,[],[f47]) ).
fof(f51,axiom,
! [X0,X1] : typeCorrect(assign(low(X0),X1)) = notb(secret(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_035) ).
fof(f52,axiom,
! [X0,X1] : typeCorrect(seq(X0,X1)) = andb(typeCorrect(X0),typeCorrect(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_036) ).
fof(f53,axiom,
! [X2,X0,X1] : typeCorrect(ifThenElse(X0,X1,X2)) = andb(typeCorrect(X1),typeCorrect(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_037) ).
fof(f54,axiom,
! [X0,X1] : prop(X0,X1) = impl(typeCorrect(X0),eq5(elem(l,run(X1,X0)),elem(l,run(cons(h,X1),X0)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_038) ).
fof(f59,axiom,
eq5(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_041) ).
fof(f60,plain,
bfalse = eq5(bfalse,btrue),
inference(reorient_equations,[],[f59]) ).
fof(f67,axiom,
! [X0,X1] : eq3(var(X0),var(X1)) = eq2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_045) ).
fof(f68,plain,
! [X0,X1] : eq2(X0,X1) = eq3(var(X0),var(X1)),
inference(reorient_equations,[],[f67]) ).
fof(f144,axiom,
! [X0] : eq3(X0,X0) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_084) ).
fof(f145,plain,
! [X0] : btrue = eq3(X0,X0),
inference(reorient_equations,[],[f144]) ).
fof(f148,axiom,
! [X0] : eq5(X0,X0) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_086) ).
fof(f149,plain,
! [X0] : btrue = eq5(X0,X0),
inference(reorient_equations,[],[f148]) ).
fof(f150,negated_conjecture,
! [X0,X1] : eq5(prop(X0,X1),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f151,plain,
! [X0,X1] : btrue != eq5(prop(X0,X1),bfalse),
inference(reorient_equations,[],[f150]) ).
fof(f152,plain,
! [X0,X1] : prop(X0,X1) = impl(typeCorrect(X0),eq5(eval(run(X1,X0),var(l)),eval(run(cons(h,X1),X0),var(l)))),
inference(definition_unfolding,[],[f54,f42,f42]) ).
fof(f154,plain,
! [X0] : bfalse = eval(nil,var(X0)),
inference(definition_unfolding,[],[f29,f42]) ).
fof(f155,plain,
! [X2,X0,X1] : eval(cons(X1,X2),var(X0)) = orb(eq3(var(X1),var(X0)),eval(X2,var(X0))),
inference(definition_unfolding,[],[f30,f42,f68,f42]) ).
fof(f167,plain,
! [X0,X1] : btrue != eq5(impl(typeCorrect(X0),eq5(eval(run(X1,X0),var(l)),eval(run(cons(h,X1),X0),var(l)))),bfalse),
inference(definition_unfolding,[],[f151,f152]) ).
fof(f189,plain,
! [X0] : notb(secret(X0)) = typeCorrect(assign(l,X0)),
inference(superposition,[],[f51,f23]) ).
fof(f233,plain,
! [X0] : typeCorrect(seq(X0,skip)) = andb(typeCorrect(X0),btrue),
inference(superposition,[],[f52,f48]) ).
fof(f324,plain,
! [X2,X0,X1] : typeCorrect(ifThenElse(X0,X1,X2)) = typeCorrect(seq(X1,X2)),
inference(forward_demodulation,[],[f53,f52]) ).
fof(f327,plain,
! [X2,X3,X0,X1] : btrue != eq5(impl(typeCorrect(seq(X0,X1)),eq5(eval(run(X3,ifThenElse(X2,X0,X1)),var(l)),eval(run(cons(h,X3),ifThenElse(X2,X0,X1)),var(l)))),bfalse),
inference(superposition,[],[f167,f324]) ).
fof(f330,plain,
! [X0,X1] : run(X0,assign(X1,tT)) = aux2(X0,X1,tT,btrue),
inference(superposition,[],[f44,f39]) ).
fof(f335,plain,
! [X0,X1] : cons(X1,X0) = run(X0,assign(X1,tT)),
inference(forward_demodulation,[],[f330,f3]) ).
fof(f420,plain,
! [X2,X0,X1] : run(nil,ifThenElse(var(X0),X1,X2)) = aux3(nil,var(X0),X1,X2,bfalse),
inference(superposition,[],[f46,f154]) ).
fof(f421,plain,
! [X2,X0,X1] : run(nil,ifThenElse(var(X0),X1,X2)) = run(nil,X2),
inference(forward_demodulation,[],[f420,f6]) ).
fof(f521,plain,
! [X0,X1] : eval(cons(X0,X1),var(X0)) = orb(btrue,eval(X1,var(X0))),
inference(superposition,[],[f155,f145]) ).
fof(f523,plain,
! [X0,X1] : btrue = eval(cons(X0,X1),var(X0)),
inference(forward_demodulation,[],[f521,f8]) ).
fof(f958,plain,
! [X2,X3,X0,X1] : run(cons(X0,X1),ifThenElse(var(X0),X2,X3)) = aux3(cons(X0,X1),var(X0),X2,X3,btrue),
inference(superposition,[],[f46,f523]) ).
fof(f964,plain,
! [X2,X3,X0,X1] : run(cons(X0,X1),ifThenElse(var(X0),X2,X3)) = run(cons(X0,X1),X2),
inference(forward_demodulation,[],[f958,f5]) ).
fof(f1000,plain,
! [X0] : andb(notb(secret(X0)),btrue) = typeCorrect(seq(assign(l,X0),skip)),
inference(superposition,[],[f233,f189]) ).
fof(f1500,plain,
! [X2,X0,X1] : btrue != eq5(impl(typeCorrect(seq(X1,X0)),eq5(eval(run(nil,X0),var(l)),eval(run(cons(h,nil),ifThenElse(var(X2),X1,X0)),var(l)))),bfalse),
inference(superposition,[],[f327,f421]) ).
fof(f9531,plain,
! [X0,X1] : btrue != eq5(impl(andb(notb(secret(X0)),btrue),eq5(eval(run(nil,skip),var(l)),eval(run(cons(h,nil),ifThenElse(var(X1),assign(l,X0),skip)),var(l)))),bfalse),
inference(superposition,[],[f1500,f1000]) ).
fof(f9589,plain,
! [X0,X1] : btrue != eq5(impl(andb(notb(secret(X0)),btrue),eq5(eval(nil,var(l)),eval(run(cons(h,nil),ifThenElse(var(X1),assign(l,X0),skip)),var(l)))),bfalse),
inference(forward_demodulation,[],[f9531,f43]) ).
fof(f9597,plain,
! [X0,X1] : btrue != eq5(impl(andb(notb(secret(X0)),btrue),eq5(bfalse,eval(run(cons(h,nil),ifThenElse(var(X1),assign(l,X0),skip)),var(l)))),bfalse),
inference(forward_demodulation,[],[f9589,f154]) ).
fof(f30517,plain,
! [X0] : btrue != eq5(impl(andb(notb(bfalse),btrue),eq5(bfalse,eval(run(cons(h,nil),ifThenElse(var(X0),assign(l,tT),skip)),var(l)))),bfalse),
inference(superposition,[],[f9597,f16]) ).
fof(f30521,plain,
! [X0] : btrue != eq5(impl(andb(btrue,btrue),eq5(bfalse,eval(run(cons(h,nil),ifThenElse(var(X0),assign(l,tT),skip)),var(l)))),bfalse),
inference(forward_demodulation,[],[f30517,f22]) ).
fof(f30532,plain,
! [X0] : btrue != eq5(impl(btrue,eq5(bfalse,eval(run(cons(h,nil),ifThenElse(var(X0),assign(l,tT),skip)),var(l)))),bfalse),
inference(forward_demodulation,[],[f30521,f34]) ).
fof(f30543,plain,
! [X0] : btrue != eq5(eq5(bfalse,eval(run(cons(h,nil),ifThenElse(var(X0),assign(l,tT),skip)),var(l))),bfalse),
inference(forward_demodulation,[],[f30532,f24]) ).
fof(f60910,plain,
btrue != eq5(eq5(bfalse,eval(run(cons(h,nil),assign(l,tT)),var(l))),bfalse),
inference(superposition,[],[f30543,f964]) ).
fof(f60911,plain,
btrue != eq5(eq5(bfalse,eval(cons(l,cons(h,nil)),var(l))),bfalse),
inference(forward_demodulation,[],[f60910,f335]) ).
fof(f60912,plain,
btrue != eq5(eq5(bfalse,btrue),bfalse),
inference(forward_demodulation,[],[f60911,f523]) ).
fof(f60913,plain,
btrue != eq5(bfalse,bfalse),
inference(forward_demodulation,[],[f60912,f60]) ).
fof(f60914,plain,
$false,
inference(forward_subsumption_resolution,[],[f60913,f149]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX240-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.26 % Computer : n010.cluster.edu
% 0.11/0.26 % Model : x86_64 x86_64
% 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.26 % Memory : 8046.5625MB
% 0.11/0.26 % OS : Linux 6.8.0-71-generic
% 0.11/0.26 % CPULimit : 300
% 0.11/0.26 % WCLimit : 300
% 0.11/0.26 % DateTime : Mon Sep 28 15:18:32 UTC 2026
% 0.11/0.26 % CPUTime :
% 0.11/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.25/0.31 Running first-order model finding
% 0.25/0.31 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.16/3.37 % (2002152)Will run a generic schedule for satisfiability detection.
% 21.16/3.37 % (2002160)dis+10_1_sil=32000:sp=arity:random_seed=2694318638:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 21.16/3.37 % (2002159)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2770858948:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 21.16/3.37 % (2002158)% WARNING: option uhcvi not known.
% 21.16/3.37 % (2002157)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1691346488_2999 on theBenchmark for (2999ds/0Mi)
% 21.16/3.37 % (2002158)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=464813658:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 21.16/3.37 % (2002163)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=911054694:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 21.16/3.37 % (2002161)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1405827343:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 21.16/3.37 % (2002162)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4176193963:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 21.16/3.37 % TRYING [1]
% 21.16/3.37 % TRYING [2]
% 21.16/3.37 % TRYING [3]
% 21.16/3.37 % (2002160)Instruction limit reached!
% 21.16/3.37 % (2002160)------------------------------
% 21.16/3.37 % (2002160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002160)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002160)Termination reason: Instruction limit
% 21.16/3.37 % (2002160)Termination phase: Saturation
% 21.16/3.37 % (2002160)Time elapsed: 0.052 s
% 21.16/3.37 % (2002160)Peak memory usage: 12 MB
% 21.16/3.37 % (2002160)Instructions burned: 103 (million)
% 21.16/3.37 % (2002171)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1538605930:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 21.16/3.37 % TRYING [4]
% 21.16/3.37 % TRYING [1]
% 21.16/3.37 % TRYING [2]
% 21.16/3.37 % (2002161)Instruction limit reached!
% 21.16/3.37 % (2002161)------------------------------
% 21.16/3.37 % (2002161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002161)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002161)Termination reason: Instruction limit
% 21.16/3.37 % (2002161)Termination phase: Saturation
% 21.16/3.37 % (2002161)Time elapsed: 0.109 s
% 21.16/3.37 % (2002161)Peak memory usage: 13 MB
% 21.16/3.37 % (2002161)Instructions burned: 116 (million)
% 21.16/3.37 % TRYING [3]
% 21.16/3.37 % (2002162)Instruction limit reached!
% 21.16/3.37 % (2002162)------------------------------
% 21.16/3.37 % (2002162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002162)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002162)Termination reason: Instruction limit
% 21.16/3.37 % (2002162)Termination phase: Saturation
% 21.16/3.37 % (2002162)Time elapsed: 0.119 s
% 21.16/3.37 % (2002162)Peak memory usage: 12 MB
% 21.16/3.37 % (2002162)Instructions burned: 131 (million)
% 21.16/3.37 % (2002173)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2215776050:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 21.16/3.37 % (2002174)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=2820339642:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 21.16/3.37 % (2002163)Instruction limit reached!
% 21.16/3.37 % (2002163)------------------------------
% 21.16/3.37 % (2002163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002163)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002163)Termination reason: Instruction limit
% 21.16/3.37 % (2002163)Termination phase: Saturation
% 21.16/3.37 % (2002163)Time elapsed: 0.152 s
% 21.16/3.37 % (2002163)Peak memory usage: 13 MB
% 21.16/3.37 % (2002163)Instructions burned: 159 (million)
% 21.16/3.37 % TRYING [4]
% 21.16/3.37 % (2002177)ott-21_1_sil=16000:fs=off:random_seed=2619854434:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 21.16/3.37 % TRYING [5]
% 21.16/3.37 % (2002173)Instruction limit reached!
% 21.16/3.37 % (2002173)------------------------------
% 21.16/3.37 % (2002173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002173)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002173)Termination reason: Instruction limit
% 21.16/3.37 % (2002173)Termination phase: Saturation
% 21.16/3.37 % (2002173)Time elapsed: 0.140 s
% 21.16/3.37 % (2002173)Peak memory usage: 13 MB
% 21.16/3.37 % (2002173)Instructions burned: 131 (million)
% 21.16/3.37 % (2002179)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=537526945:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 21.16/3.37 % (2002177)Instruction limit reached!
% 21.16/3.37 % (2002177)------------------------------
% 21.16/3.37 % (2002177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002177)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002177)Termination reason: Instruction limit
% 21.16/3.37 % (2002177)Termination phase: Saturation
% 21.16/3.37 % (2002177)Time elapsed: 0.164 s
% 21.16/3.37 % (2002177)Peak memory usage: 12 MB
% 21.16/3.37 % (2002177)Instructions burned: 181 (million)
% 21.16/3.37 % (2002181)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=607849489:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 21.16/3.37 % TRYING [1]
% 21.16/3.37 % TRYING [2]
% 21.16/3.37 % TRYING [3]
% 21.16/3.37 % TRYING [5]
% 21.16/3.37 % (2002174)Instruction limit reached!
% 21.16/3.37 % (2002174)------------------------------
% 21.16/3.37 % (2002174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002174)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002174)Termination reason: Instruction limit
% 21.16/3.37 % (2002174)Termination phase: Saturation
% 21.16/3.37 % (2002174)Time elapsed: 0.333 s
% 21.16/3.37 % (2002174)Peak memory usage: 19 MB
% 21.16/3.37 % (2002174)Instructions burned: 684 (million)
% 21.16/3.37 % (2002183)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2491043992:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 21.16/3.37 % TRYING [4]
% 21.16/3.37 % (2002171)Instruction limit reached!
% 21.16/3.37 % (2002171)------------------------------
% 21.16/3.37 % (2002171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002171)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002171)Termination reason: Instruction limit
% 21.16/3.37 % (2002171)Termination phase: Finite model building constraint generation
% 21.16/3.37 % (2002171)Time elapsed: 0.519 s
% 21.16/3.37 % (2002171)Peak memory usage: 30 MB
% 21.16/3.37 % (2002171)Instructions burned: 714 (million)
% 21.16/3.37 % (2002185)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=824062434:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 21.16/3.37 % (2002179)Instruction limit reached!
% 21.16/3.37 % (2002179)------------------------------
% 21.16/3.37 % (2002179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002179)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002179)Termination reason: Instruction limit
% 21.16/3.37 % (2002179)Termination phase: Saturation
% 21.16/3.37 % (2002179)Time elapsed: 0.480 s
% 21.16/3.37 % (2002179)Peak memory usage: 17 MB
% 21.16/3.37 % (2002179)Instructions burned: 478 (million)
% 21.16/3.37 % (2002187)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=733916553: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)
% 21.16/3.37 % TRYING [6]
% 21.16/3.37 % (2002181)Instruction limit reached!
% 21.16/3.37 % (2002181)------------------------------
% 21.16/3.37 % (2002181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002181)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002181)Termination reason: Instruction limit
% 21.16/3.37 % (2002181)Termination phase: Finite model building SAT solving
% 21.16/3.37 % (2002181)Time elapsed: 0.642 s
% 21.16/3.37 % (2002181)Peak memory usage: 27 MB
% 21.16/3.37 % (2002181)Instructions burned: 865 (million)
% 21.16/3.37 % (2002189)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2853824727:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 21.16/3.37 % (2002183)Instruction limit reached!
% 21.16/3.37 % (2002183)------------------------------
% 21.16/3.37 % (2002183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002183)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002183)Termination reason: Instruction limit
% 21.16/3.37 % (2002183)Termination phase: Saturation
% 21.16/3.37 % (2002183)Time elapsed: 0.628 s
% 21.16/3.37 % (2002183)Peak memory usage: 22 MB
% 21.16/3.37 % (2002183)Instructions burned: 1180 (million)
% 21.16/3.37 % (2002191)fmb+10_1_sil=64000:random_seed=663569256:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 21.16/3.37 % TRYING [1]
% 21.16/3.37 % TRYING [2]
% 21.16/3.37 % TRYING [3]
% 21.16/3.37 % TRYING [4]
% 21.16/3.37 % (2002185)Instruction limit reached!
% 21.16/3.37 % (2002185)------------------------------
% 21.16/3.37 % (2002185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002185)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002185)Termination reason: Instruction limit
% 21.16/3.37 % (2002185)Termination phase: Finite model building constraint generation
% 21.16/3.37 % (2002185)Time elapsed: 0.807 s
% 21.16/3.37 % (2002185)Peak memory usage: 106 MB
% 21.16/3.37 % (2002185)Instructions burned: 889 (million)
% 21.16/3.37 % (2002187)Instruction limit reached!
% 21.16/3.37 % (2002187)------------------------------
% 21.16/3.37 % (2002187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002187)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002187)Termination reason: Instruction limit
% 21.16/3.37 % (2002187)Termination phase: Saturation
% 21.16/3.37 % (2002187)Time elapsed: 0.627 s
% 21.16/3.37 % (2002187)Peak memory usage: 18 MB
% 21.16/3.37 % (2002187)Instructions burned: 692 (million)
% 21.16/3.37 % (2002193)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3998601767:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 21.16/3.37 % (2002194)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2525364759:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 21.16/3.37 % TRYING [20]
% 21.16/3.37 % TRYING [8]
% 21.16/3.37 % TRYING [5]
% 21.16/3.37 % (2002189)Instruction limit reached!
% 21.16/3.37 % (2002189)------------------------------
% 21.16/3.37 % (2002189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002189)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002189)Termination reason: Instruction limit
% 21.16/3.37 % (2002189)Termination phase: Saturation
% 21.16/3.37 % (2002189)Time elapsed: 0.808 s
% 21.16/3.37 % (2002189)Peak memory usage: 19 MB
% 21.16/3.37 % (2002189)Instructions burned: 880 (million)
% 21.16/3.37 % (2002197)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2958016181:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 21.16/3.37 % (2002194)Instruction limit reached!
% 21.16/3.37 % (2002194)------------------------------
% 21.16/3.37 % (2002194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.37 % (2002194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.37 % (2002194)CaDiCaL version: 2.1.3
% 21.16/3.37 % (2002194)Termination reason: Instruction limit
% 21.16/3.37 % (2002194)Termination phase: Finite model building constraint generation
% 21.16/3.37 % (2002194)Time elapsed: 0.667 s
% 21.16/3.37 % (2002194)Peak memory usage: 73 MB
% 21.16/3.37 % (2002194)Instructions burned: 920 (million)
% 21.16/3.37 % (2002199)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=689883931:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 21.16/3.37 % TRYING [7]
% 21.16/3.37 % TRYING [6]
% 21.16/3.37 % (2002158) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2002152-2002158"...
% 21.16/3.37 % (2002158)...printing done.
% 21.16/3.37 % (2002158)Refutation found. Thanks to Tanya!
% 21.16/3.37 % SZS status Unsatisfiable for theBenchmark
% 21.16/3.37 % SZS output start Proof for theBenchmark
% See solution above
% 21.16/3.38 % (2002158)------------------------------
% 21.16/3.38 % (2002158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.16/3.38 % (2002158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.16/3.38 % (2002158)CaDiCaL version: 2.1.3
% 21.16/3.38 % (2002158)Termination reason: Refutation
% 21.16/3.38 % (2002158)Time elapsed: 2.961 s
% 21.16/3.38 % (2002158)Peak memory usage: 49 MB
% 21.16/3.38 % (2002158)Instructions burned: 3237 (million)
% 21.16/3.38 % (2002152)Success in time 3.055 s
% 21.16/3.38 % Vampire exiting
%------------------------------------------------------------------------------