%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP048-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:16:30 AM UTC 2026
% Result : Unsatisfiable 15.25s 2.66s
% Output : Refutation 15.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 9
% Syntax : Number of formulae : 58 ( 58 unt; 0 def)
% Number of atoms : 58 ( 57 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-4 aty)
% Number of variables : 104 ( 104 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X0] : product(identity,X0,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).
fof(f3,axiom,
! [X0] : product(inverse(X0),X0,identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_inverse) ).
fof(f4,plain,
! [X0] : true = product(inverse(X0),X0,identity),
inference(reorient_equations,[],[f3]) ).
fof(f7,axiom,
! [X2,X3,X0,X1] : ifeq(product(X0,X1,X2),true,ifeq(product(X0,X1,X3),true,equalish(X3,X2),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',total_function2) ).
fof(f8,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X0,X1,X3),true,equalish(X3,X2),true),true),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X4,X5] : ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(product(X5,X3,X0),true,product(X5,X4,X2),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity1) ).
fof(f10,plain,
! [X2,X3,X0,X1,X4,X5] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(product(X5,X3,X0),true,product(X5,X4,X2),true),true),true),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X4,X5] : ifeq(product(X0,X1,X2),true,ifeq(product(X3,X2,X4),true,ifeq(product(X3,X0,X5),true,product(X5,X1,X4),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity2) ).
fof(f12,plain,
! [X2,X3,X0,X1,X4,X5] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X3,X2,X4),true,ifeq(product(X3,X0,X5),true,product(X5,X1,X4),true),true),true),
inference(reorient_equations,[],[f11]) ).
fof(f13,axiom,
! [X2,X3,X0,X1] : ifeq(equalish(X0,X1),true,ifeq(product(X2,X3,X0),true,product(X2,X3,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_substitution3) ).
fof(f14,plain,
! [X2,X3,X0,X1] : true = ifeq(equalish(X0,X1),true,ifeq(product(X2,X3,X0),true,product(X2,X3,X1),true),true),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
equalish(a,b) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_equals_b) ).
fof(f16,plain,
true = equalish(a,b),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
equalish(inverse(a),inverse(b)) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_inverse_substitution) ).
fof(f18,plain,
true != equalish(inverse(a),inverse(b)),
inference(reorient_equations,[],[f17]) ).
fof(f19,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(product(identity,X0,X1),true,equalish(X1,X0),true),true),
inference(superposition,[],[f8,f2]) ).
fof(f30,plain,
! [X0,X1] : true = ifeq(equalish(X0,X1),true,ifeq(true,true,product(identity,X0,X1),true),true),
inference(superposition,[],[f14,f2]) ).
fof(f38,plain,
! [X0,X1] : true = ifeq(equalish(X0,X1),true,product(identity,X0,X1),true),
inference(forward_demodulation,[],[f30,f1]) ).
fof(f48,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,X2),true,ifeq(true,true,ifeq(product(X3,inverse(X1),X0),true,product(X3,identity,X2),true),true),true),
inference(superposition,[],[f10,f4]) ).
fof(f51,plain,
! [X2,X3,X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(product(X2,X0,X3),true,ifeq(true,true,product(inverse(X2),X3,X1),true),true),true),
inference(superposition,[],[f10,f4]) ).
fof(f57,plain,
! [X2,X3,X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(product(X2,X0,X3),true,product(inverse(X2),X3,X1),true),true),
inference(forward_demodulation,[],[f51,f1]) ).
fof(f60,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X3,inverse(X1),X0),true,product(X3,identity,X2),true),true),
inference(forward_demodulation,[],[f48,f1]) ).
fof(f68,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,X2),true,ifeq(true,true,ifeq(product(inverse(X2),X0,X3),true,product(X3,X1,identity),true),true),true),
inference(superposition,[],[f12,f4]) ).
fof(f80,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,X2),true,ifeq(product(inverse(X2),X0,X3),true,product(X3,X1,identity),true),true),
inference(forward_demodulation,[],[f68,f1]) ).
fof(f87,plain,
true = ifeq(true,true,product(identity,a,b),true),
inference(superposition,[],[f38,f16]) ).
fof(f104,plain,
true = product(identity,a,b),
inference(superposition,[],[f87,f1]) ).
fof(f147,plain,
true = ifeq(true,true,ifeq(true,true,equalish(b,a),true),true),
inference(superposition,[],[f19,f104]) ).
fof(f154,plain,
true = ifeq(true,true,equalish(b,a),true),
inference(forward_demodulation,[],[f147,f1]) ).
fof(f158,plain,
true = equalish(b,a),
inference(superposition,[],[f154,f1]) ).
fof(f175,plain,
true = ifeq(true,true,product(identity,b,a),true),
inference(superposition,[],[f38,f158]) ).
fof(f215,plain,
true = product(identity,b,a),
inference(superposition,[],[f175,f1]) ).
fof(f375,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(product(X1,X0,X2),true,product(inverse(X1),X2,X0),true),true),
inference(superposition,[],[f57,f2]) ).
fof(f380,plain,
! [X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(true,true,product(inverse(inverse(X0)),identity,X1),true),true),
inference(superposition,[],[f57,f4]) ).
fof(f390,plain,
! [X0,X1] : true = ifeq(product(identity,X0,X1),true,product(inverse(inverse(X0)),identity,X1),true),
inference(forward_demodulation,[],[f380,f1]) ).
fof(f393,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(product(X1,inverse(X0),identity),true,product(X1,identity,X0),true),true),
inference(superposition,[],[f60,f2]) ).
fof(f444,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(product(inverse(X0),identity,X1),true,product(X1,X0,identity),true),true),
inference(superposition,[],[f80,f2]) ).
fof(f1521,plain,
! [X0] : true = ifeq(true,true,product(inverse(inverse(X0)),identity,X0),true),
inference(superposition,[],[f390,f2]) ).
fof(f1524,plain,
true = ifeq(true,true,product(inverse(inverse(b)),identity,a),true),
inference(superposition,[],[f390,f215]) ).
fof(f2896,plain,
! [X2,X0,X1] : true = ifeq(product(X0,X1,X2),true,product(inverse(X0),X2,X1),true),
inference(superposition,[],[f375,f1]) ).
fof(f2959,plain,
! [X0] : true = product(inverse(inverse(X0)),identity,X0),
inference(superposition,[],[f1521,f1]) ).
fof(f3211,plain,
! [X0] : true = ifeq(true,true,ifeq(true,true,product(X0,inverse(X0),identity),true),true),
inference(superposition,[],[f444,f2959]) ).
fof(f3223,plain,
! [X0,X1] : true = ifeq(product(inverse(X0),identity,X1),true,product(X1,X0,identity),true),
inference(superposition,[],[f444,f1]) ).
fof(f3232,plain,
! [X0] : true = ifeq(true,true,product(X0,inverse(X0),identity),true),
inference(forward_demodulation,[],[f3211,f1]) ).
fof(f3288,plain,
! [X0] : true = product(X0,inverse(X0),identity),
inference(superposition,[],[f3232,f1]) ).
fof(f3292,plain,
! [X0] : true = ifeq(true,true,ifeq(true,true,product(X0,identity,X0),true),true),
inference(superposition,[],[f393,f3288]) ).
fof(f3482,plain,
! [X0] : true = ifeq(true,true,product(X0,identity,X0),true),
inference(forward_demodulation,[],[f3292,f1]) ).
fof(f3488,plain,
! [X0] : true = product(X0,identity,X0),
inference(superposition,[],[f3482,f1]) ).
fof(f3554,plain,
! [X0,X1] : true = ifeq(product(X0,identity,X1),true,ifeq(true,true,equalish(X0,X1),true),true),
inference(superposition,[],[f8,f3488]) ).
fof(f3713,plain,
! [X0,X1] : true = ifeq(product(X0,identity,X1),true,equalish(X0,X1),true),
inference(forward_demodulation,[],[f3554,f1]) ).
fof(f18385,plain,
true = product(inverse(inverse(b)),identity,a),
inference(superposition,[],[f1524,f1]) ).
fof(f18412,plain,
true = ifeq(true,true,product(a,inverse(b),identity),true),
inference(superposition,[],[f3223,f18385]) ).
fof(f18651,plain,
true = product(a,inverse(b),identity),
inference(superposition,[],[f18412,f1]) ).
fof(f18786,plain,
true = ifeq(true,true,product(inverse(a),identity,inverse(b)),true),
inference(superposition,[],[f2896,f18651]) ).
fof(f39058,plain,
true = product(inverse(a),identity,inverse(b)),
inference(superposition,[],[f18786,f1]) ).
fof(f39090,plain,
true = ifeq(true,true,equalish(inverse(a),inverse(b)),true),
inference(superposition,[],[f3713,f39058]) ).
fof(f39989,plain,
true = equalish(inverse(a),inverse(b)),
inference(superposition,[],[f1,f39090]) ).
fof(f39990,plain,
$false,
inference(forward_subsumption_resolution,[],[f39989,f18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP048-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.40 % Computer : n004.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 09:16:22 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.43 Running first-order model finding
% 0.13/0.43 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
% 13.97/2.46 % (3238168)Will run a generic schedule for satisfiability detection.
% 13.97/2.46 % (3238178)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2455072533:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 13.97/2.46 % (3238174)% WARNING: option uhcvi not known.
% 13.97/2.46 % (3238173)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3803474766_3000 on theBenchmark for (3000ds/0Mi)
% 13.97/2.46 % (3238174)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=663891127:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 13.97/2.46 % (3238176)dis+10_1_sil=32000:sp=arity:random_seed=1877397227:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 13.97/2.46 % (3238175)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=576959043:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 13.97/2.46 % (3238177)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=906825846:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 13.97/2.46 % (3238179)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1827853689:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 13.97/2.46 % TRYING [1]
% 13.97/2.46 % TRYING [2]
% 13.97/2.46 % TRYING [3]
% 13.97/2.46 % (3238178)Instruction limit reached!
% 13.97/2.46 % (3238178)------------------------------
% 13.97/2.46 % (3238178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.46 % (3238178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.46 % (3238178)CaDiCaL version: 2.1.3
% 13.97/2.46 % (3238178)Termination reason: Instruction limit
% 13.97/2.46 % (3238178)Termination phase: Saturation
% 13.97/2.46 % (3238178)Time elapsed: 0.042 s
% 13.97/2.46 % (3238178)Peak memory usage: 13 MB
% 13.97/2.46 % (3238178)Instructions burned: 133 (million)
% 13.97/2.46 % (3238187)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3227007441:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.97/2.46 % TRYING [1]
% 13.97/2.46 % TRYING [2]
% 13.97/2.46 % TRYING [3]
% 13.97/2.46 % (3238176)Instruction limit reached!
% 13.97/2.46 % (3238176)------------------------------
% 13.97/2.46 % (3238176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.46 % (3238176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.46 % (3238176)CaDiCaL version: 2.1.3
% 13.97/2.46 % (3238176)Termination reason: Instruction limit
% 13.97/2.46 % (3238176)Termination phase: Saturation
% 13.97/2.46 % (3238176)Time elapsed: 0.057 s
% 13.97/2.46 % (3238176)Peak memory usage: 12 MB
% 13.97/2.46 % (3238176)Instructions burned: 104 (million)
% 13.97/2.46 % TRYING [4]
% 13.97/2.46 % (3238177)Instruction limit reached!
% 13.97/2.46 % (3238177)------------------------------
% 13.97/2.46 % (3238177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.46 % (3238177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.46 % (3238177)CaDiCaL version: 2.1.3
% 13.97/2.46 % (3238177)Termination reason: Instruction limit
% 13.97/2.46 % (3238177)Termination phase: Saturation
% 13.97/2.46 % (3238177)Time elapsed: 0.067 s
% 13.97/2.46 % (3238177)Peak memory usage: 13 MB
% 13.97/2.46 % (3238177)Instructions burned: 117 (million)
% 13.97/2.46 % (3238189)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3825760053:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 13.97/2.46 % TRYING [4]
% 13.97/2.46 % (3238190)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=2853510219:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 13.97/2.46 % (3238179)Instruction limit reached!
% 13.97/2.46 % (3238179)------------------------------
% 13.97/2.46 % (3238179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.46 % (3238179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.97/2.46 % (3238179)CaDiCaL version: 2.1.3
% 13.97/2.46 % (3238179)Termination reason: Instruction limit
% 13.97/2.46 % (3238179)Termination phase: Saturation
% 13.97/2.46 % (3238179)Time elapsed: 0.095 s
% 13.97/2.46 % (3238179)Peak memory usage: 12 MB
% 13.97/2.46 % (3238179)Instructions burned: 160 (million)
% 13.97/2.46 % (3238193)ott-21_1_sil=16000:fs=off:random_seed=216765037:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.97/2.46 % (3238189)Instruction limit reached!
% 13.97/2.46 % (3238189)------------------------------
% 13.97/2.46 % (3238189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.97/2.46 % (3238189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238189)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238189)Termination reason: Instruction limit
% 15.25/2.66 % (3238189)Termination phase: Saturation
% 15.25/2.66 % (3238189)Time elapsed: 0.082 s
% 15.25/2.66 % (3238189)Peak memory usage: 13 MB
% 15.25/2.66 % (3238189)Instructions burned: 131 (million)
% 15.25/2.66 % (3238195)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3793587023:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 15.25/2.66 % (3238187)Instruction limit reached!
% 15.25/2.66 % (3238187)------------------------------
% 15.25/2.66 % (3238187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238187)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238187)Termination reason: Instruction limit
% 15.25/2.66 % (3238187)Termination phase: Finite model building constraint generation
% 15.25/2.66 % (3238187)Time elapsed: 0.137 s
% 15.25/2.66 % (3238187)Peak memory usage: 37 MB
% 15.25/2.66 % (3238187)Instructions burned: 714 (million)
% 15.25/2.66 % (3238197)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=997606594:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 15.25/2.66 % TRYING [1]
% 15.25/2.66 % TRYING [2]
% 15.25/2.66 % TRYING [3]
% 15.25/2.66 % (3238193)Instruction limit reached!
% 15.25/2.66 % (3238193)------------------------------
% 15.25/2.66 % (3238193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238193)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238193)Termination reason: Instruction limit
% 15.25/2.66 % (3238193)Termination phase: Saturation
% 15.25/2.66 % (3238193)Time elapsed: 0.095 s
% 15.25/2.66 % (3238193)Peak memory usage: 12 MB
% 15.25/2.66 % (3238193)Instructions burned: 181 (million)
% 15.25/2.66 % (3238199)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1953613252:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 15.25/2.66 % TRYING [4]
% 15.25/2.66 % (3238197)Instruction limit reached!
% 15.25/2.66 % (3238197)------------------------------
% 15.25/2.66 % (3238197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238197)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238197)Termination reason: Instruction limit
% 15.25/2.66 % (3238197)Termination phase: Finite model building SAT solving
% 15.25/2.66 % (3238197)Time elapsed: 0.190 s
% 15.25/2.66 % (3238197)Peak memory usage: 43 MB
% 15.25/2.66 % (3238197)Instructions burned: 871 (million)
% 15.25/2.66 % (3238201)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2929021174:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 15.25/2.66 % (3238195)Instruction limit reached!
% 15.25/2.66 % (3238195)------------------------------
% 15.25/2.66 % (3238195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238195)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238195)Termination reason: Instruction limit
% 15.25/2.66 % (3238195)Termination phase: Saturation
% 15.25/2.66 % (3238195)Time elapsed: 0.249 s
% 15.25/2.66 % (3238195)Peak memory usage: 16 MB
% 15.25/2.66 % (3238195)Instructions burned: 477 (million)
% 15.25/2.66 % (3238203)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=3663178774:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 15.25/2.66 % (3238190)Instruction limit reached!
% 15.25/2.66 % (3238190)------------------------------
% 15.25/2.66 % (3238190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238190)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238190)Termination reason: Instruction limit
% 15.25/2.66 % (3238190)Termination phase: Saturation
% 15.25/2.66 % (3238190)Time elapsed: 0.367 s
% 15.25/2.66 % (3238190)Peak memory usage: 20 MB
% 15.25/2.66 % (3238190)Instructions burned: 685 (million)
% 15.25/2.66 % (3238205)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2941121858:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 15.25/2.66 % TRYING [5]
% 15.25/2.66 % (3238201)Instruction limit reached!
% 15.25/2.66 % (3238201)------------------------------
% 15.25/2.66 % (3238201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238201)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238201)Termination reason: Instruction limit
% 15.25/2.66 % (3238201)Termination phase: Finite model building constraint generation
% 15.25/2.66 % (3238201)Time elapsed: 0.230 s
% 15.25/2.66 % (3238201)Peak memory usage: 104 MB
% 15.25/2.66 % (3238201)Instructions burned: 894 (million)
% 15.25/2.66 % (3238207)fmb+10_1_sil=64000:random_seed=188070768:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 15.25/2.66 % TRYING [1]
% 15.25/2.66 % TRYING [2]
% 15.25/2.66 % TRYING [3]
% 15.25/2.66 % TRYING [4]
% 15.25/2.66 % (3238203)Instruction limit reached!
% 15.25/2.66 % (3238203)------------------------------
% 15.25/2.66 % (3238203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238203)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238203)Termination reason: Instruction limit
% 15.25/2.66 % (3238203)Termination phase: Saturation
% 15.25/2.66 % (3238203)Time elapsed: 0.400 s
% 15.25/2.66 % (3238203)Peak memory usage: 21 MB
% 15.25/2.66 % (3238203)Instructions burned: 692 (million)
% 15.25/2.66 % (3238209)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3876238872:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 15.25/2.66 % TRYING [20]
% 15.25/2.66 % (3238199)Instruction limit reached!
% 15.25/2.66 % (3238199)------------------------------
% 15.25/2.66 % (3238199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238199)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238199)Termination reason: Instruction limit
% 15.25/2.66 % (3238199)Termination phase: Saturation
% 15.25/2.66 % (3238199)Time elapsed: 0.680 s
% 15.25/2.66 % (3238199)Peak memory usage: 31 MB
% 15.25/2.66 % (3238199)Instructions burned: 1180 (million)
% 15.25/2.66 % (3238211)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1996118325:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 15.25/2.66 % TRYING [8]
% 15.25/2.66 % (3238205)Instruction limit reached!
% 15.25/2.66 % (3238205)------------------------------
% 15.25/2.66 % (3238205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238205)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238205)Termination reason: Instruction limit
% 15.25/2.66 % (3238205)Termination phase: Saturation
% 15.25/2.66 % (3238205)Time elapsed: 0.464 s
% 15.25/2.66 % (3238205)Peak memory usage: 20 MB
% 15.25/2.66 % (3238205)Instructions burned: 880 (million)
% 15.25/2.66 % (3238213)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1690099914:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 15.25/2.66 % (3238211)Instruction limit reached!
% 15.25/2.66 % (3238211)------------------------------
% 15.25/2.66 % (3238211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238211)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238211)Termination reason: Instruction limit
% 15.25/2.66 % (3238211)Termination phase: Finite model building constraint generation
% 15.25/2.66 % (3238211)Time elapsed: 0.330 s
% 15.25/2.66 % (3238211)Peak memory usage: 74 MB
% 15.25/2.66 % (3238211)Instructions burned: 921 (million)
% 15.25/2.66 % TRYING [5]
% 15.25/2.66 % (3238215)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2547721798:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 15.25/2.66 % (3238215)Instruction limit reached!
% 15.25/2.66 % (3238215)------------------------------
% 15.25/2.66 % (3238215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238215)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238215)Termination reason: Instruction limit
% 15.25/2.66 % (3238215)Termination phase: Saturation
% 15.25/2.66 % (3238215)Time elapsed: 0.685 s
% 15.25/2.66 % (3238215)Peak memory usage: 27 MB
% 15.25/2.66 % (3238215)Instructions burned: 1473 (million)
% 15.25/2.66 % (3238217)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=394354913:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 15.25/2.66 % (3238217)Cannot represent all propositional literals internally
% 15.25/2.66 % (3238217)Refutation not found, incomplete strategy
% 15.25/2.66 % (3238217)------------------------------
% 15.25/2.66 % (3238217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238217)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238217)Termination reason: Refutation not found, incomplete strategy
% 15.25/2.66 % (3238217)Time elapsed: 0.003 s
% 15.25/2.66 % (3238217)Peak memory usage: 10 MB
% 15.25/2.66 % (3238217)Instructions burned: 4 (million)
% 15.25/2.66 % (3238217)------------------------------
% 15.25/2.66 % (3238217)------------------------------
% 15.25/2.66 % (3238219)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4181580337:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 15.25/2.66 % TRYING [16]
% 15.25/2.66 % (3238213) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3238168-3238213"...
% 15.25/2.66 % (3238213)...printing done.
% 15.25/2.66 % (3238213)Refutation found. Thanks to Tanya!
% 15.25/2.66 % SZS status Unsatisfiable for theBenchmark
% 15.25/2.66 % SZS output start Proof for theBenchmark
% See solution above
% 15.25/2.66 % (3238213)------------------------------
% 15.25/2.66 % (3238213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.25/2.66 % (3238213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.66 % (3238213)CaDiCaL version: 2.1.3
% 15.25/2.66 % (3238213)Termination reason: Refutation
% 15.25/2.66 % (3238213)Time elapsed: 1.190 s
% 15.25/2.66 % (3238213)Peak memory usage: 31 MB
% 15.25/2.66 % (3238213)Instructions burned: 2124 (million)
% 15.25/2.66 % (3238168)Success in time 2.221 s
% 15.25/2.66 % Vampire exiting
%------------------------------------------------------------------------------