%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG004-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:35:40 PM UTC 2026
% Result : Unsatisfiable 54.28s 14.44s
% Output : Refutation 54.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 18
% Syntax : Number of formulae : 69 ( 35 unt; 0 def)
% Number of atoms : 137 ( 20 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 137 ( 69 ~; 68 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 138 ( 138 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : sum(additive_identity,X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',additive_identity1) ).
fof(f2,axiom,
! [X0] : sum(X0,additive_identity,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',additive_identity2) ).
fof(f3,axiom,
! [X0,X1] : product(X0,X1,multiply(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',closure_of_multiplication) ).
fof(f4,axiom,
! [X0,X1] : sum(X0,X1,add(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',closure_of_addition) ).
fof(f5,axiom,
! [X0] : sum(additive_inverse(X0),X0,additive_identity),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',left_inverse) ).
fof(f6,axiom,
! [X0] : sum(X0,additive_inverse(X0),additive_identity),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',right_inverse) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X2,X3,X5)
| ~ sum(X1,X3,X4)
| ~ sum(X0,X1,X2)
| sum(X0,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',associativity_of_addition1) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X0,X4,X5)
| ~ sum(X1,X3,X4)
| ~ sum(X0,X1,X2)
| sum(X2,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',associativity_of_addition2) ).
fof(f9,axiom,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| sum(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',commutativity_of_addition) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X0,X5,X6)
| ~ product(X0,X3,X4)
| ~ sum(X1,X3,X5)
| ~ product(X0,X1,X2)
| sum(X2,X4,X6) ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',distributivity1) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X0,X1,X2)
| ~ product(X0,X3,X4)
| ~ sum(X1,X3,X5)
| ~ sum(X2,X4,X6)
| product(X0,X5,X6) ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',distributivity2) ).
fof(f14,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X5,X1,X6)
| ~ product(X3,X1,X4)
| ~ sum(X0,X3,X5)
| ~ product(X0,X1,X2)
| sum(X2,X4,X6) ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',distributivity3) ).
fof(f15,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X0,X1,X2)
| ~ product(X3,X1,X4)
| ~ sum(X0,X3,X5)
| ~ sum(X2,X4,X6)
| product(X5,X1,X6) ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',distributivity4) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ sum(X0,X1,X3)
| ~ sum(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',addition_is_well_defined) ).
fof(f17,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',multiplication_is_well_defined) ).
fof(f18,axiom,
product(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_times_b) ).
fof(f19,axiom,
product(additive_inverse(a),additive_inverse(b),d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_inverse_times_b_inverse) ).
fof(f20,negated_conjecture,
c != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_c_equals_d) ).
fof(f21,plain,
! [X0,X1] :
( ~ sum(additive_identity,X0,X1)
| X0 = X1 ),
inference(resolution,[],[f16,f1]) ).
fof(f22,plain,
! [X0,X1] :
( ~ sum(X0,additive_identity,X1)
| X0 = X1 ),
inference(resolution,[],[f16,f2]) ).
fof(f39,plain,
! [X2,X3,X0,X1] :
( ~ product(additive_inverse(a),X2,X3)
| ~ sum(X2,X0,additive_inverse(b))
| ~ product(additive_inverse(a),X0,X1)
| sum(X3,X1,d) ),
inference(resolution,[],[f12,f19]) ).
fof(f44,plain,
! [X0] : add(additive_identity,X0) = X0,
inference(resolution,[],[f21,f4]) ).
fof(f46,plain,
! [X2,X3,X0,X1] :
( ~ product(additive_inverse(a),X0,X1)
| ~ sum(additive_inverse(b),X0,X2)
| ~ sum(d,X1,X3)
| product(additive_inverse(a),X2,X3) ),
inference(resolution,[],[f13,f19]) ).
fof(f50,plain,
! [X2,X3,X0,X1] :
( ~ product(X2,b,X3)
| ~ sum(X2,X0,a)
| ~ product(X0,b,X1)
| sum(X3,X1,c) ),
inference(resolution,[],[f14,f18]) ).
fof(f54,plain,
! [X2,X3,X0,X1] :
( ~ product(X0,b,X1)
| ~ sum(a,X0,X2)
| ~ sum(c,X1,X3)
| product(X2,b,X3) ),
inference(resolution,[],[f15,f18]) ).
fof(f60,plain,
! [X0] : add(X0,additive_identity) = X0,
inference(resolution,[],[f22,f4]) ).
fof(f65,plain,
! [X0,X1] : sum(X0,X1,add(X1,X0)),
inference(resolution,[],[f9,f4]) ).
fof(f72,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| add(X1,X0) = X2 ),
inference(resolution,[],[f65,f16]) ).
fof(f132,plain,
! [X0,X1] :
( ~ sum(a,X0,a)
| ~ product(X0,b,X1)
| sum(c,X1,c) ),
inference(resolution,[],[f50,f18]) ).
fof(f136,plain,
! [X2,X0,X1] :
( ~ sum(c,multiply(X0,b),X2)
| ~ sum(a,X0,X1)
| product(X1,b,X2) ),
inference(resolution,[],[f54,f3]) ).
fof(f142,plain,
! [X2,X3,X0,X1] :
( ~ sum(X3,X0,additive_identity)
| ~ sum(X0,X1,X2)
| sum(X3,X2,X1) ),
inference(resolution,[],[f7,f1]) ).
fof(f145,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,additive_inverse(X1),X2)
| ~ sum(X3,X0,X1)
| sum(X3,X2,additive_identity) ),
inference(resolution,[],[f7,f6]) ).
fof(f156,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,X1,additive_identity)
| ~ sum(X2,X0,X3)
| sum(X3,X1,X2) ),
inference(resolution,[],[f8,f2]) ).
fof(f157,plain,
! [X2,X3,X0,X1] :
( ~ sum(additive_inverse(X2),X0,X3)
| ~ sum(X0,X1,X2)
| sum(X3,X1,additive_identity) ),
inference(resolution,[],[f8,f5]) ).
fof(f165,plain,
! [X0,X1] :
( ~ sum(additive_inverse(b),X0,additive_inverse(b))
| ~ product(additive_inverse(a),X0,X1)
| sum(d,X1,d) ),
inference(resolution,[],[f39,f19]) ).
fof(f172,plain,
! [X2,X0,X1] :
( ~ sum(d,multiply(additive_inverse(a),X0),X2)
| ~ sum(additive_inverse(b),X0,X1)
| product(additive_inverse(a),X1,X2) ),
inference(resolution,[],[f46,f3]) ).
fof(f185,plain,
! [X0] :
( ~ product(additive_identity,b,X0)
| sum(c,X0,c) ),
inference(resolution,[],[f132,f2]) ).
fof(f186,plain,
sum(c,multiply(additive_identity,b),c),
inference(resolution,[],[f185,f3]) ).
fof(f193,plain,
sum(multiply(additive_identity,b),c,c),
inference(resolution,[],[f186,f9]) ).
fof(f196,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| sum(additive_inverse(X0),X2,X1) ),
inference(resolution,[],[f142,f5]) ).
fof(f233,plain,
! [X2,X0,X1] :
( ~ sum(X0,additive_inverse(X1),X2)
| sum(X2,X1,X0) ),
inference(resolution,[],[f156,f5]) ).
fof(f260,plain,
! [X0,X1] :
( ~ sum(X0,X1,X1)
| sum(X0,additive_identity,additive_identity) ),
inference(resolution,[],[f145,f6]) ).
fof(f268,plain,
sum(multiply(additive_identity,b),additive_identity,additive_identity),
inference(resolution,[],[f260,f193]) ).
fof(f270,plain,
! [X0,X1] :
( ~ sum(X0,X1,X0)
| sum(additive_identity,X1,additive_identity) ),
inference(resolution,[],[f157,f5]) ).
fof(f301,plain,
! [X0] :
( ~ product(additive_inverse(a),additive_identity,X0)
| sum(d,X0,d) ),
inference(resolution,[],[f165,f2]) ).
fof(f317,plain,
additive_identity = multiply(additive_identity,b),
inference(resolution,[],[f268,f22]) ).
fof(f336,plain,
product(additive_identity,b,additive_identity),
inference(superposition,[],[f3,f317]) ).
fof(f348,plain,
! [X0] :
( ~ product(additive_identity,b,X0)
| additive_identity = X0 ),
inference(resolution,[],[f336,f17]) ).
fof(f377,plain,
sum(d,multiply(additive_inverse(a),additive_identity),d),
inference(resolution,[],[f301,f3]) ).
fof(f401,plain,
sum(additive_identity,multiply(additive_inverse(a),additive_identity),additive_identity),
inference(resolution,[],[f377,f270]) ).
fof(f417,plain,
! [X0,X1] : sum(additive_inverse(X0),add(X0,X1),X1),
inference(resolution,[],[f196,f4]) ).
fof(f483,plain,
! [X0,X1] : sum(add(X0,additive_inverse(X1)),X1,X0),
inference(resolution,[],[f233,f4]) ).
fof(f633,plain,
! [X0,X1] : add(add(X0,X1),additive_inverse(X0)) = X1,
inference(resolution,[],[f417,f72]) ).
fof(f749,plain,
! [X0,X1] : add(X0,add(X1,additive_inverse(X0))) = X1,
inference(resolution,[],[f483,f72]) ).
fof(f847,plain,
additive_identity = multiply(additive_inverse(a),additive_identity),
inference(resolution,[],[f401,f21]) ).
fof(f883,plain,
product(additive_inverse(a),additive_identity,additive_identity),
inference(superposition,[],[f3,f847]) ).
fof(f908,plain,
! [X0] :
( ~ product(additive_inverse(a),additive_identity,X0)
| additive_identity = X0 ),
inference(resolution,[],[f883,f17]) ).
fof(f1793,plain,
! [X0,X1] :
( ~ sum(a,X0,X1)
| product(X1,b,add(c,multiply(X0,b))) ),
inference(resolution,[],[f136,f4]) ).
fof(f2141,plain,
! [X0,X1] :
( ~ sum(additive_inverse(b),X0,X1)
| product(additive_inverse(a),X1,add(d,multiply(additive_inverse(a),X0))) ),
inference(resolution,[],[f172,f4]) ).
fof(f7043,plain,
product(additive_identity,b,add(c,multiply(additive_inverse(a),b))),
inference(resolution,[],[f1793,f6]) ).
fof(f10968,plain,
additive_identity = add(c,multiply(additive_inverse(a),b)),
inference(resolution,[],[f7043,f348]) ).
fof(f11051,plain,
add(additive_identity,additive_inverse(c)) = multiply(additive_inverse(a),b),
inference(superposition,[],[f633,f10968]) ).
fof(f11105,plain,
additive_inverse(c) = multiply(additive_inverse(a),b),
inference(forward_demodulation,[],[f11051,f44]) ).
fof(f12533,plain,
product(additive_inverse(a),additive_identity,add(d,multiply(additive_inverse(a),b))),
inference(resolution,[],[f2141,f5]) ).
fof(f12563,plain,
product(additive_inverse(a),additive_identity,add(d,additive_inverse(c))),
inference(forward_demodulation,[],[f12533,f11105]) ).
fof(f12578,plain,
additive_identity = add(d,additive_inverse(c)),
inference(resolution,[],[f12563,f908]) ).
fof(f12646,plain,
d = add(c,additive_identity),
inference(superposition,[],[f749,f12578]) ).
fof(f12727,plain,
c = d,
inference(forward_demodulation,[],[f12646,f60]) ).
fof(f12751,plain,
$false,
inference(global_subsumption,[],[f12727,f20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG004-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.39 % Computer : n016.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sun Sep 27 23:03:02 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.18/0.45 Running first-order model finding
% 0.18/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 28.61/4.51 % (3092255)Will run a generic schedule for satisfiability detection.
% 28.61/4.51 % (3092260)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1657127295_2999 on theBenchmark for (2999ds/0Mi)
% 28.61/4.51 % TRYING [1]
% 28.61/4.51 % TRYING [2]
% 28.61/4.51 % TRYING [3]
% 28.61/4.51 % (3092261)% WARNING: option uhcvi not known.
% 28.61/4.51 % TRYING [4]
% 28.61/4.51 % (3092262)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2986380360:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 28.61/4.51 % (3092263)dis+10_1_sil=32000:sp=arity:random_seed=1471007344:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 28.61/4.51 % (3092264)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2491794473:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 28.61/4.51 % (3092265)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2786741974:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 28.61/4.51 % (3092266)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=885356589:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 28.61/4.51 % (3092261)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2908444854:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 28.61/4.51 % TRYING [5]
% 28.61/4.51 % (3092264)Instruction limit reached!
% 28.61/4.51 % (3092264)------------------------------
% 28.61/4.51 % (3092264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.61/4.51 % (3092264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.61/4.51 % (3092264)CaDiCaL version: 2.1.3
% 28.61/4.51 % (3092264)Termination reason: Instruction limit
% 28.61/4.51 % (3092264)Termination phase: Saturation
% 28.61/4.51 % (3092264)Time elapsed: 0.101 s
% 28.61/4.51 % (3092264)Peak memory usage: 12 MB
% 28.61/4.51 % (3092264)Instructions burned: 116 (million)
% 28.61/4.51 % (3092263)Instruction limit reached!
% 28.61/4.51 % (3092263)------------------------------
% 28.61/4.51 % (3092263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.61/4.51 % (3092263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.61/4.51 % (3092263)CaDiCaL version: 2.1.3
% 28.61/4.51 % (3092263)Termination reason: Instruction limit
% 28.61/4.51 % (3092263)Termination phase: Saturation
% 28.61/4.51 % (3092263)Time elapsed: 0.107 s
% 28.61/4.51 % (3092263)Peak memory usage: 12 MB
% 28.61/4.51 % (3092263)Instructions burned: 103 (million)
% 28.61/4.51 % (3092265)Instruction limit reached!
% 28.61/4.51 % (3092265)------------------------------
% 28.61/4.51 % (3092265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.61/4.51 % (3092265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.61/4.51 % (3092265)CaDiCaL version: 2.1.3
% 28.61/4.51 % (3092265)Termination reason: Instruction limit
% 28.61/4.51 % (3092265)Termination phase: Saturation
% 28.61/4.51 % (3092265)Time elapsed: 0.130 s
% 28.61/4.51 % (3092265)Peak memory usage: 12 MB
% 28.61/4.51 % (3092265)Instructions burned: 132 (million)
% 28.61/4.51 % TRYING [6]
% 28.61/4.51 % (3092274)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2315733011:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 28.61/4.51 % TRYING [1]
% 28.61/4.51 % TRYING [2]
% 28.61/4.51 % (3092275)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4040240185:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 28.61/4.51 % TRYING [3]
% 28.61/4.51 % (3092266)Instruction limit reached!
% 28.61/4.51 % (3092266)------------------------------
% 28.61/4.51 % (3092266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.61/4.51 % (3092266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.61/4.51 % (3092266)CaDiCaL version: 2.1.3
% 28.61/4.51 % (3092266)Termination reason: Instruction limit
% 28.61/4.51 % (3092266)Termination phase: Saturation
% 28.61/4.51 % (3092266)Time elapsed: 0.160 s
% 28.61/4.51 % (3092266)Peak memory usage: 12 MB
% 28.61/4.51 % (3092266)Instructions burned: 160 (million)
% 28.61/4.51 % TRYING [4]
% 28.61/4.51 % (3092276)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=2332893356:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 28.61/4.51 % (3092279)ott-21_1_sil=16000:fs=off:random_seed=1425653886:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 28.61/4.51 % TRYING [5]
% 28.61/4.51 % (3092275)Instruction limit reached!
% 28.61/4.51 % (3092275)------------------------------
% 28.61/4.51 % (3092275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.40/12.07 % (3092275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.40/12.07 % (3092275)CaDiCaL version: 2.1.3
% 82.40/12.07 % (3092275)Termination reason: Instruction limit
% 82.40/12.07 % (3092275)Termination phase: Saturation
% 82.40/12.07 % (3092275)Time elapsed: 0.143 s
% 82.40/12.07 % (3092275)Peak memory usage: 12 MB
% 82.40/12.07 % (3092275)Instructions burned: 132 (million)
% 82.40/12.07 % (3092282)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2111350857:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 82.40/12.07 % (3092279)Instruction limit reached!
% 82.40/12.07 % (3092279)------------------------------
% 82.40/12.07 % (3092279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.40/12.07 % (3092279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.40/12.07 % (3092279)CaDiCaL version: 2.1.3
% 82.40/12.07 % (3092279)Termination reason: Instruction limit
% 82.40/12.07 % (3092279)Termination phase: Saturation
% 82.40/12.07 % (3092279)Time elapsed: 0.162 s
% 82.40/12.07 % (3092279)Peak memory usage: 12 MB
% 82.40/12.07 % (3092279)Instructions burned: 181 (million)
% 82.40/12.07 % TRYING [7]
% 82.40/12.07 % (3092284)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1362047711:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 82.40/12.07 % TRYING [1]
% 82.40/12.07 % TRYING [2]
% 82.40/12.07 % TRYING [3]
% 82.40/12.07 % TRYING [4]
% 82.40/12.07 % TRYING [6]
% 82.40/12.07 % TRYING [5]
% 82.40/12.07 % (3092274)Instruction limit reached!
% 82.40/12.07 % (3092274)------------------------------
% 82.40/12.07 % (3092274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.40/12.07 % (3092274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.40/12.07 % (3092274)CaDiCaL version: 2.1.3
% 82.40/12.07 % (3092274)Termination reason: Instruction limit
% 82.40/12.07 % (3092274)Termination phase: Finite model building constraint generation
% 82.40/12.07 % (3092274)Time elapsed: 0.524 s
% 82.40/12.07 % (3092274)Peak memory usage: 28 MB
% 82.40/12.07 % (3092274)Instructions burned: 714 (million)
% 82.40/12.07 % (3092286)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2308445358:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 82.40/12.07 % (3092276)Instruction limit reached!
% 82.40/12.07 % (3092276)------------------------------
% 82.40/12.07 % (3092276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.40/12.07 % (3092276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.40/12.07 % (3092276)CaDiCaL version: 2.1.3
% 82.40/12.07 % (3092276)Termination reason: Instruction limit
% 82.40/12.07 % (3092276)Termination phase: Saturation
% 82.40/12.07 % (3092276)Time elapsed: 0.637 s
% 82.40/12.07 % (3092276)Peak memory usage: 15 MB
% 82.40/12.07 % (3092276)Instructions burned: 684 (million)
% 82.40/12.07 % (3092282)Instruction limit reached!
% 82.40/12.07 % (3092282)------------------------------
% 82.40/12.07 % (3092282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.40/12.07 % (3092282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.40/12.07 % (3092282)CaDiCaL version: 2.1.3
% 82.40/12.07 % (3092282)Termination reason: Instruction limit
% 82.40/12.07 % (3092282)Termination phase: Saturation
% 82.40/12.07 % (3092282)Time elapsed: 0.522 s
% 82.40/12.07 % (3092282)Peak memory usage: 12 MB
% 82.40/12.07 % (3092282)Instructions burned: 477 (million)
% 82.40/12.07 % (3092288)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2464336967:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 82.40/12.07 % TRYING [6]
% 82.40/12.07 % (3092289)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=2901050413:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 82.40/12.07 % (3092284)Instruction limit reached!
% 82.40/12.07 % (3092284)------------------------------
% 82.40/12.07 % (3092284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.40/12.07 % (3092284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.40/12.07 % (3092284)CaDiCaL version: 2.1.3
% 82.40/12.07 % (3092284)Termination reason: Instruction limit
% 82.40/12.07 % (3092284)Termination phase: Finite model building constraint generation
% 82.40/12.07 % (3092284)Time elapsed: 0.589 s
% 82.40/12.07 % (3092284)Peak memory usage: 24 MB
% 82.40/12.07 % (3092284)Instructions burned: 865 (million)
% 82.40/12.07 % TRYING [8]
% 82.40/12.07 % (3092292)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=344169510:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 54.28/14.43 % TRYING [14]
% 54.28/14.43 % (3092288)Instruction limit reached!
% 54.28/14.43 % (3092288)------------------------------
% 54.28/14.43 % (3092288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092288)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092288)Termination reason: Instruction limit
% 54.28/14.43 % (3092288)Termination phase: Finite model building constraint generation
% 54.28/14.43 % (3092288)Time elapsed: 0.718 s
% 54.28/14.43 % (3092288)Peak memory usage: 93 MB
% 54.28/14.43 % (3092288)Instructions burned: 889 (million)
% 54.28/14.43 % (3092289)Instruction limit reached!
% 54.28/14.43 % (3092289)------------------------------
% 54.28/14.43 % (3092289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092289)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092289)Termination reason: Instruction limit
% 54.28/14.43 % (3092289)Termination phase: Saturation
% 54.28/14.43 % (3092289)Time elapsed: 0.689 s
% 54.28/14.43 % (3092289)Peak memory usage: 16 MB
% 54.28/14.43 % (3092289)Instructions burned: 692 (million)
% 54.28/14.43 % (3092295)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1167529120:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 54.28/14.43 % TRYING [20]
% 54.28/14.43 % (3092294)fmb+10_1_sil=64000:random_seed=3738011561:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi)
% 54.28/14.43 % TRYING [1]
% 54.28/14.43 % TRYING [2]
% 54.28/14.43 % TRYING [3]
% 54.28/14.43 % TRYING [4]
% 54.28/14.43 % TRYING [5]
% 54.28/14.43 % (3092292)Instruction limit reached!
% 54.28/14.43 % (3092292)------------------------------
% 54.28/14.43 % (3092292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092292)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092292)Termination reason: Instruction limit
% 54.28/14.43 % (3092292)Termination phase: Saturation
% 54.28/14.43 % (3092292)Time elapsed: 0.823 s
% 54.28/14.43 % (3092292)Peak memory usage: 14 MB
% 54.28/14.43 % (3092292)Instructions burned: 880 (million)
% 54.28/14.43 % (3092286)Instruction limit reached!
% 54.28/14.43 % (3092286)------------------------------
% 54.28/14.43 % (3092286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092286)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092286)Termination reason: Instruction limit
% 54.28/14.43 % (3092286)Termination phase: Saturation
% 54.28/14.43 % (3092286)Time elapsed: 1.177 s
% 54.28/14.43 % (3092286)Peak memory usage: 16 MB
% 54.28/14.43 % (3092286)Instructions burned: 1179 (million)
% 54.28/14.43 % (3092298)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2578094579:fmbsr=1.7:i=920_2980 on theBenchmark for (2980ds/920Mi)
% 54.28/14.43 % TRYING [8]
% 54.28/14.43 % (3092299)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2947853417:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 54.28/14.43 % TRYING [6]
% 54.28/14.43 % TRYING [9]
% 54.28/14.43 % (3092298)Instruction limit reached!
% 54.28/14.43 % (3092298)------------------------------
% 54.28/14.43 % (3092298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092298)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092298)Termination reason: Instruction limit
% 54.28/14.43 % (3092298)Termination phase: Finite model building constraint generation
% 54.28/14.43 % (3092298)Time elapsed: 0.668 s
% 54.28/14.43 % (3092298)Peak memory usage: 77 MB
% 54.28/14.43 % (3092298)Instructions burned: 920 (million)
% 54.28/14.43 % (3092302)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1973254969:i=1472:ins=7:fdi=8:gsp=on_2973 on theBenchmark for (2973ds/1472Mi)
% 54.28/14.43 % TRYING [7]
% 54.28/14.43 % (3092302)Instruction limit reached!
% 54.28/14.43 % (3092302)------------------------------
% 54.28/14.43 % (3092302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092302)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092302)Termination reason: Instruction limit
% 54.28/14.43 % (3092302)Termination phase: Saturation
% 54.28/14.43 % (3092302)Time elapsed: 1.266 s
% 54.28/14.43 % (3092302)Peak memory usage: 23 MB
% 54.28/14.43 % (3092302)Instructions burned: 1473 (million)
% 54.28/14.43 % (3092304)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2303767753:i=6324_2959 on theBenchmark for (2959ds/6324Mi)
% 54.28/14.43 % TRYING [77]
% 54.28/14.43 % TRYING [10]
% 54.28/14.43 % TRYING [8]
% 54.28/14.43 % (3092299)Instruction limit reached!
% 54.28/14.43 % (3092299)------------------------------
% 54.28/14.43 % (3092299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092299)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092299)Termination reason: Instruction limit
% 54.28/14.43 % (3092299)Termination phase: Saturation
% 54.28/14.43 % (3092299)Time elapsed: 4.331 s
% 54.28/14.43 % (3092299)Peak memory usage: 19 MB
% 54.28/14.43 % (3092299)Instructions burned: 5132 (million)
% 54.28/14.43 % (3092306)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1172232166:fmbsr=2.30978:i=2174_2936 on theBenchmark for (2936ds/2174Mi)
% 54.28/14.43 % TRYING [16]
% 54.28/14.43 % (3092306)Instruction limit reached!
% 54.28/14.43 % (3092306)------------------------------
% 54.28/14.43 % (3092306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092306)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092306)Termination reason: Instruction limit
% 54.28/14.43 % (3092306)Termination phase: Finite model building constraint generation
% 54.28/14.43 % (3092306)Time elapsed: 1.396 s
% 54.28/14.43 % (3092306)Peak memory usage: 131 MB
% 54.28/14.43 % (3092306)Instructions burned: 2175 (million)
% 54.28/14.43 % (3092308)ott-2_1_sil=16000:newcnf=on:random_seed=1079946677:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2921 on theBenchmark for (2921ds/869Mi)
% 54.28/14.43 % TRYING [11]
% 54.28/14.43 % (3092295)Instruction limit reached!
% 54.28/14.43 % (3092295)------------------------------
% 54.28/14.43 % (3092295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092295)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092295)Termination reason: Instruction limit
% 54.28/14.43 % (3092295)Termination phase: Finite model building constraint generation
% 54.28/14.43 % (3092295)Time elapsed: 6.617 s
% 54.28/14.43 % (3092295)Peak memory usage: 664 MB
% 54.28/14.43 % (3092295)Instructions burned: 9516 (million)
% 54.28/14.43 % (3092304)Instruction limit reached!
% 54.28/14.43 % (3092304)------------------------------
% 54.28/14.43 % (3092304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092304)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092304)Termination reason: Instruction limit
% 54.28/14.43 % (3092304)Termination phase: Finite model building constraint generation
% 54.28/14.43 % (3092304)Time elapsed: 4.369 s
% 54.28/14.43 % (3092304)Peak memory usage: 449 MB
% 54.28/14.43 % (3092304)Instructions burned: 6324 (million)
% 54.28/14.43 % (3092310)ott+10_1_sil=32000:tgt=ground:random_seed=4100463962:i=5114:av=off_2915 on theBenchmark for (2915ds/5114Mi)
% 54.28/14.43 % (3092308)Instruction limit reached!
% 54.28/14.43 % (3092308)------------------------------
% 54.28/14.43 % (3092308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092308)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092308)Termination reason: Instruction limit
% 54.28/14.43 % (3092308)Termination phase: Saturation
% 54.28/14.43 % (3092308)Time elapsed: 0.713 s
% 54.28/14.43 % (3092308)Peak memory usage: 13 MB
% 54.28/14.43 % (3092308)Instructions burned: 870 (million)
% 54.28/14.43 % (3092311)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1664037020:i=54282_2914 on theBenchmark for (2914ds/54282Mi)
% 54.28/14.43 % TRYING [1]
% 54.28/14.43 % TRYING [2]
% 54.28/14.43 % TRYING [3]
% 54.28/14.43 % TRYING [4]
% 54.28/14.43 % (3092314)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2477282184:i=3512:aac=none_2914 on theBenchmark for (2914ds/3512Mi)
% 54.28/14.43 % TRYING [5]
% 54.28/14.43 % TRYING [6]
% 54.28/14.43 % TRYING [7]
% 54.28/14.43 % TRYING [9]
% 54.28/14.43 % TRYING [8]
% 54.28/14.43 % (3092314)Instruction limit reached!
% 54.28/14.43 % (3092314)------------------------------
% 54.28/14.43 % (3092314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.43 % (3092314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.43 % (3092314)CaDiCaL version: 2.1.3
% 54.28/14.43 % (3092314)Termination reason: Instruction limit
% 54.28/14.43 % (3092314)Termination phase: Saturation
% 54.28/14.43 % (3092314)Time elapsed: 2.976 s
% 54.28/14.43 % (3092314)Peak memory usage: 18 MB
% 54.28/14.44 % (3092314)Instructions burned: 3514 (million)
% 54.28/14.44 % (3092316)dis+21_1_sil=32000:sas=cadical:random_seed=3322999803:i=3773:amm=off_2883 on theBenchmark for (2883ds/3773Mi)
% 54.28/14.44 % TRYING [9]
% 54.28/14.44 % TRYING [12]
% 54.28/14.44 % (3092310)Instruction limit reached!
% 54.28/14.44 % (3092310)------------------------------
% 54.28/14.44 % (3092310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.44 % (3092310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.44 % (3092310)CaDiCaL version: 2.1.3
% 54.28/14.44 % (3092310)Termination reason: Instruction limit
% 54.28/14.44 % (3092310)Termination phase: Saturation
% 54.28/14.44 % (3092310)Time elapsed: 4.895 s
% 54.28/14.44 % (3092310)Peak memory usage: 23 MB
% 54.28/14.44 % (3092310)Instructions burned: 5114 (million)
% 54.28/14.44 % (3092318)ott+11_1_sil=16000:gs=on:random_seed=3811334394:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2865 on theBenchmark for (2865ds/2251Mi)
% 54.28/14.44 % (3092318) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3092255-3092318"...
% 54.28/14.44 % (3092318)...printing done.
% 54.28/14.44 % (3092318)Refutation found. Thanks to Tanya!
% 54.28/14.44 % SZS status Unsatisfiable for theBenchmark
% 54.28/14.44 % SZS output start Proof for theBenchmark
% See solution above
% 54.28/14.44 % (3092318)------------------------------
% 54.28/14.44 % (3092318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.28/14.44 % (3092318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.28/14.44 % (3092318)CaDiCaL version: 2.1.3
% 54.28/14.44 % (3092318)Termination reason: Refutation
% 54.28/14.44 % (3092318)Time elapsed: 0.382 s
% 54.28/14.44 % (3092318)Peak memory usage: 14 MB
% 54.28/14.44 % (3092318)Instructions burned: 372 (million)
% 54.28/14.44 % (3092255)Success in time 13.973 s
% 54.28/14.44 % Vampire exiting
%------------------------------------------------------------------------------