%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW178+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:39:34 PM UTC 2026
% Result : Theorem 20.63s 3.27s
% Output : Refutation 20.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 42 ( 32 unt; 5 def)
% Number of atoms : 52 ( 19 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 21 ( 11 ~; 7 |; 0 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-3 aty)
% Number of variables : 31 ( 31 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0,X1,X2] :
( class_Groups_Ogroup__add(X2)
=> c_Groups_Ominus__class_Ominus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0),X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__diff__cancel) ).
fof(f38,axiom,
! [X0,X1,X2] :
( class_RealVector_Oreal__normed__vector(X2)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),c_RealVector_Onorm__class_Onorm(X2,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_norm__triangle__ineq4) ).
fof(f102,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__1(X2)
=> c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(f1137,axiom,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Ocomm__semiring__1) ).
fof(f1169,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(f1189,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ogroup__add) ).
fof(f1200,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1201,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
inference(negated_conjecture,[status(cth)],[f1200]) ).
fof(f1208,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
inference(flattening,[],[f1201]) ).
fof(f1259,plain,
! [X0,X1,X2] :
( c_Groups_Ominus__class_Ominus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0),X0) = X1
| ~ class_Groups_Ogroup__add(X2) ),
inference(ennf_transformation,[],[f28]) ).
fof(f1269,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),c_RealVector_Onorm__class_Onorm(X2,X0)))
| ~ class_RealVector_Oreal__normed__vector(X2) ),
inference(ennf_transformation,[],[f38]) ).
fof(f1346,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1)
| ~ class_Rings_Ocomm__semiring__1(X2) ),
inference(ennf_transformation,[],[f102]) ).
fof(f2580,plain,
! [X2,X0,X1] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Ominus__class_Ominus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f1259]) ).
fof(f2590,plain,
! [X2,X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),c_RealVector_Onorm__class_Onorm(X2,X0)))
| ~ class_RealVector_Oreal__normed__vector(X2) ),
inference(cnf_transformation,[],[f1269]) ).
fof(f2666,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X2)
| c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
inference(cnf_transformation,[],[f1346]) ).
fof(f4053,plain,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1137]) ).
fof(f4085,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1169]) ).
fof(f4105,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1189]) ).
fof(f4116,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
inference(cnf_transformation,[],[f1208]) ).
fof(f4425,definition,
sF66 = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),
introduced(definition,[new_symbols(definition,[sF66])],[function_definition]) ).
fof(f4426,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w) = sF66,
inference(reorient_equations,[],[f4425]) ).
fof(f4427,definition,
sF67 = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z),
introduced(definition,[new_symbols(definition,[sF67])],[function_definition]) ).
fof(f4428,plain,
c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z) = sF67,
inference(reorient_equations,[],[f4427]) ).
fof(f4429,definition,
sF68 = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sF67),
introduced(definition,[new_symbols(definition,[sF68])],[function_definition]) ).
fof(f4430,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sF67) = sF68,
inference(reorient_equations,[],[f4429]) ).
fof(f4431,definition,
sF69 = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z),
introduced(definition,[new_symbols(definition,[sF69])],[function_definition]) ).
fof(f4432,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z) = sF69,
inference(reorient_equations,[],[f4431]) ).
fof(f4433,definition,
sF70 = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,sF68,sF69),
introduced(definition,[new_symbols(definition,[sF70])],[function_definition]) ).
fof(f4434,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,sF68,sF69) = sF70,
inference(reorient_equations,[],[f4433]) ).
fof(f4435,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF66,sF70),
inference(definition_folding,[],[f4116,f4434,f4432,f4430,f4428,f4426]) ).
fof(f5665,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1),X1) = X0,
inference(resolution,[],[f2580,f4105]) ).
fof(f5824,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0),
inference(resolution,[],[f2666,f4053]) ).
fof(f7010,plain,
v_w = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,sF67,v_z),
inference(superposition,[],[f5665,f4428]) ).
fof(f30702,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sF67),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z)))
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(superposition,[],[f2590,f7010]) ).
fof(f30823,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sF67),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
inference(forward_subsumption_resolution,[],[f30702,f4085]) ).
fof(f30903,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sF67))),
inference(forward_demodulation,[],[f30823,f5824]) ).
fof(f30940,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z),sF68)),
inference(forward_demodulation,[],[f30903,f4430]) ).
fof(f30952,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,sF68,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
inference(forward_demodulation,[],[f30940,f5824]) ).
fof(f30958,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,sF68,sF69)),
inference(forward_demodulation,[],[f30952,f4432]) ).
fof(f30961,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),sF70),
inference(forward_demodulation,[],[f30958,f4434]) ).
fof(f30964,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF66,sF70),
inference(forward_demodulation,[],[f30961,f4426]) ).
fof(f30965,plain,
$false,
inference(forward_subsumption_resolution,[],[f30964,f4435]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW178+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n007.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 13:10:25 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.25 Running first-order model finding
% 0.10/0.25 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
% 9.52/1.85 % (2386115)Will run a generic schedule for satisfiability detection.
% 9.52/1.85 % (2386123)dis+10_1_sil=32000:sp=arity:random_seed=1924059416:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 9.52/1.85 % (2386121)% WARNING: option uhcvi not known.
% 9.52/1.85 % (2386122)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1764675869:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 9.52/1.85 % (2386120)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1597797557_2999 on theBenchmark for (2999ds/0Mi)
% 9.52/1.85 % (2386124)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=571819761:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 9.52/1.85 % (2386125)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=868339485:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 9.52/1.85 % (2386126)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4278909026:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 9.52/1.85 % (2386121)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2413145317:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 9.52/1.85 % (2386123)Instruction limit reached!
% 9.52/1.85 % (2386123)------------------------------
% 9.52/1.85 % (2386123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.52/1.85 % (2386123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.52/1.85 % (2386123)CaDiCaL version: 2.1.3
% 9.52/1.85 % (2386123)Termination reason: Instruction limit
% 9.52/1.85 % (2386123)Termination phase: Saturation
% 9.52/1.85 % (2386123)Time elapsed: 0.029 s
% 9.52/1.85 % (2386123)Peak memory usage: 14 MB
% 9.52/1.85 % (2386123)Instructions burned: 104 (million)
% 9.52/1.85 % (2386134)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3127219051:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 9.52/1.85 % (2386124)Instruction limit reached!
% 9.52/1.85 % (2386124)------------------------------
% 9.52/1.85 % (2386124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.52/1.85 % (2386124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.52/1.85 % (2386124)CaDiCaL version: 2.1.3
% 9.52/1.85 % (2386124)Termination reason: Instruction limit
% 9.52/1.85 % (2386124)Termination phase: Saturation
% 9.52/1.85 % (2386124)Time elapsed: 0.057 s
% 9.52/1.85 % (2386124)Peak memory usage: 14 MB
% 9.52/1.85 % (2386124)Instructions burned: 116 (million)
% 9.52/1.85 % (2386125)Instruction limit reached!
% 9.52/1.85 % (2386125)------------------------------
% 9.52/1.85 % (2386125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.52/1.85 % (2386125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.52/1.85 % (2386125)CaDiCaL version: 2.1.3
% 9.52/1.85 % (2386125)Termination reason: Instruction limit
% 9.52/1.85 % (2386125)Termination phase: Saturation
% 9.52/1.85 % (2386125)Time elapsed: 0.069 s
% 9.52/1.85 % (2386125)Peak memory usage: 14 MB
% 9.52/1.85 % (2386125)Instructions burned: 133 (million)
% 9.52/1.85 % (2386136)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=251414527:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 9.52/1.85 % (2386137)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=3373887080:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 9.52/1.85 % (2386126)Instruction limit reached!
% 9.52/1.85 % (2386126)------------------------------
% 9.52/1.85 % (2386126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.52/1.85 % (2386126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.52/1.85 % (2386126)CaDiCaL version: 2.1.3
% 9.52/1.85 % (2386126)Termination reason: Instruction limit
% 9.52/1.85 % (2386126)Termination phase: Saturation
% 9.52/1.85 % (2386126)Time elapsed: 0.091 s
% 9.52/1.85 % (2386126)Peak memory usage: 15 MB
% 9.52/1.85 % (2386126)Instructions burned: 160 (million)
% 9.52/1.85 % (2386140)ott-21_1_sil=16000:fs=off:random_seed=2262045858:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.52/1.85 % (2386136)Instruction limit reached!
% 9.52/1.85 % (2386136)------------------------------
% 9.52/1.85 % (2386136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.52/1.85 % (2386136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.52/1.85 % (2386136)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386136)Termination reason: Instruction limit
% 20.63/3.27 % (2386136)Termination phase: Saturation
% 20.63/3.27 % (2386136)Time elapsed: 0.062 s
% 20.63/3.27 % (2386136)Peak memory usage: 14 MB
% 20.63/3.27 % (2386136)Instructions burned: 131 (million)
% 20.63/3.27 % (2386142)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2522367142:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 20.63/3.27 % TRYING [1]
% 20.63/3.27 % TRYING [2]
% 20.63/3.27 % (2386140)Instruction limit reached!
% 20.63/3.27 % (2386140)------------------------------
% 20.63/3.27 % (2386140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386140)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386140)Termination reason: Instruction limit
% 20.63/3.27 % (2386140)Termination phase: Saturation
% 20.63/3.27 % (2386140)Time elapsed: 0.092 s
% 20.63/3.27 % (2386140)Peak memory usage: 14 MB
% 20.63/3.27 % (2386140)Instructions burned: 181 (million)
% 20.63/3.27 % (2386134)Instruction limit reached!
% 20.63/3.27 % (2386134)------------------------------
% 20.63/3.27 % (2386134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386134)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386134)Termination reason: Instruction limit
% 20.63/3.27 % (2386134)Termination phase: Finite model building constraint generation
% 20.63/3.27 % (2386134)Time elapsed: 0.178 s
% 20.63/3.27 % (2386134)Peak memory usage: 25 MB
% 20.63/3.27 % (2386134)Instructions burned: 720 (million)
% 20.63/3.27 % (2386145)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2687595162:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 20.63/3.27 % (2386144)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1668047781:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 20.63/3.27 % TRYING [1]
% 20.63/3.27 % TRYING [2]
% 20.63/3.27 % (2386137)Instruction limit reached!
% 20.63/3.27 % (2386137)------------------------------
% 20.63/3.27 % (2386137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386137)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386137)Termination reason: Instruction limit
% 20.63/3.27 % (2386137)Termination phase: Saturation
% 20.63/3.27 % (2386137)Time elapsed: 0.328 s
% 20.63/3.27 % (2386137)Peak memory usage: 16 MB
% 20.63/3.27 % (2386137)Instructions burned: 684 (million)
% 20.63/3.27 % (2386148)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=596968329:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 20.63/3.27 % (2386142)Instruction limit reached!
% 20.63/3.27 % (2386142)------------------------------
% 20.63/3.27 % (2386142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386142)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386142)Termination reason: Instruction limit
% 20.63/3.27 % (2386142)Termination phase: Saturation
% 20.63/3.27 % (2386142)Time elapsed: 0.292 s
% 20.63/3.27 % (2386142)Peak memory usage: 16 MB
% 20.63/3.27 % (2386142)Instructions burned: 477 (million)
% 20.63/3.27 % (2386150)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=3940980264: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)
% 20.63/3.27 % TRYING [3]
% 20.63/3.27 % TRYING [1]
% 20.63/3.27 % TRYING [2]
% 20.63/3.27 % (2386145)Instruction limit reached!
% 20.63/3.27 % (2386145)------------------------------
% 20.63/3.27 % (2386145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386145)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386145)Termination reason: Instruction limit
% 20.63/3.27 % (2386145)Termination phase: Saturation
% 20.63/3.27 % (2386145)Time elapsed: 0.391 s
% 20.63/3.27 % (2386145)Peak memory usage: 22 MB
% 20.63/3.27 % (2386145)Instructions burned: 1180 (million)
% 20.63/3.27 % (2386152)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=466472827:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 20.63/3.27 % (2386144)Instruction limit reached!
% 20.63/3.27 % (2386144)------------------------------
% 20.63/3.27 % (2386144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386144)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386144)Termination reason: Instruction limit
% 20.63/3.27 % (2386144)Termination phase: Finite model building constraint generation
% 20.63/3.27 % (2386144)Time elapsed: 0.407 s
% 20.63/3.27 % (2386144)Peak memory usage: 34 MB
% 20.63/3.27 % (2386144)Instructions burned: 865 (million)
% 20.63/3.27 % (2386154)fmb+10_1_sil=64000:random_seed=3045249266:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 20.63/3.27 % (2386148)Instruction limit reached!
% 20.63/3.27 % (2386148)------------------------------
% 20.63/3.27 % (2386148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386148)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386148)Termination reason: Instruction limit
% 20.63/3.27 % (2386148)Termination phase: Finite model building constraint generation
% 20.63/3.27 % (2386148)Time elapsed: 0.430 s
% 20.63/3.27 % (2386148)Peak memory usage: 53 MB
% 20.63/3.27 % (2386148)Instructions burned: 891 (million)
% 20.63/3.27 % (2386152)Instruction limit reached!
% 20.63/3.27 % (2386152)------------------------------
% 20.63/3.27 % (2386152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386152)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386152)Termination reason: Instruction limit
% 20.63/3.27 % (2386152)Termination phase: Saturation
% 20.63/3.27 % (2386152)Time elapsed: 0.248 s
% 20.63/3.27 % (2386152)Peak memory usage: 21 MB
% 20.63/3.27 % (2386152)Instructions burned: 881 (million)
% 20.63/3.27 % (2386157)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2587667973:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 20.63/3.27 % (2386156)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=870108451:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 20.63/3.27 % (2386150)Instruction limit reached!
% 20.63/3.27 % (2386150)------------------------------
% 20.63/3.27 % (2386150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386150)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386150)Termination reason: Instruction limit
% 20.63/3.27 % (2386150)Termination phase: Saturation
% 20.63/3.27 % (2386150)Time elapsed: 0.427 s
% 20.63/3.27 % (2386150)Peak memory usage: 20 MB
% 20.63/3.27 % (2386150)Instructions burned: 693 (million)
% 20.63/3.27 % (2386160)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1176829990:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 20.63/3.27 % TRYING [1]
% 20.63/3.27 % TRYING [2]
% 20.63/3.27 % TRYING [8]
% 20.63/3.27 % (2386157)Instruction limit reached!
% 20.63/3.27 % (2386157)------------------------------
% 20.63/3.27 % (2386157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386157)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386157)Termination reason: Instruction limit
% 20.63/3.27 % (2386157)Termination phase: Finite model building constraint generation
% 20.63/3.27 % (2386157)Time elapsed: 0.220 s
% 20.63/3.27 % (2386157)Peak memory usage: 43 MB
% 20.63/3.27 % (2386157)Instructions burned: 922 (million)
% 20.63/3.27 % (2386162)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1524196204:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 20.63/3.27 % (2386156)Cannot represent all propositional literals internally
% 20.63/3.27 % (2386156)Refutation not found, incomplete strategy
% 20.63/3.27 % (2386156)------------------------------
% 20.63/3.27 % (2386156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386156)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386156)Termination reason: Refutation not found, incomplete strategy
% 20.63/3.27 % (2386156)Time elapsed: 0.306 s
% 20.63/3.27 % (2386156)Peak memory usage: 22 MB
% 20.63/3.27 % (2386156)Instructions burned: 625 (million)
% 20.63/3.27 % (2386156)------------------------------
% 20.63/3.27 % (2386156)------------------------------
% 20.63/3.27 % (2386164)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=992466427:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 20.63/3.27 % (2386162)Instruction limit reached!
% 20.63/3.27 % (2386162)------------------------------
% 20.63/3.27 % (2386162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386162)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386162)Termination reason: Instruction limit
% 20.63/3.27 % (2386162)Termination phase: Saturation
% 20.63/3.27 % (2386162)Time elapsed: 0.392 s
% 20.63/3.27 % (2386162)Peak memory usage: 27 MB
% 20.63/3.27 % (2386162)Instructions burned: 1474 (million)
% 20.63/3.27 % (2386166)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=511318389:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi)
% 20.63/3.27 % (2386164)Cannot represent all propositional literals internally
% 20.63/3.27 % (2386164)Refutation not found, incomplete strategy
% 20.63/3.27 % (2386164)------------------------------
% 20.63/3.27 % (2386164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386164)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386164)Termination reason: Refutation not found, incomplete strategy
% 20.63/3.27 % (2386164)Time elapsed: 0.322 s
% 20.63/3.27 % (2386164)Peak memory usage: 23 MB
% 20.63/3.27 % (2386164)Instructions burned: 662 (million)
% 20.63/3.27 % (2386164)------------------------------
% 20.63/3.27 % (2386164)------------------------------
% 20.63/3.27 % (2386168)ott-2_1_sil=16000:newcnf=on:random_seed=1353963621:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi)
% 20.63/3.27 % TRYING [4]
% 20.63/3.27 % TRYING [3]
% 20.63/3.27 % (2386168)Instruction limit reached!
% 20.63/3.27 % (2386168)------------------------------
% 20.63/3.27 % (2386168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386168)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386168)Termination reason: Instruction limit
% 20.63/3.27 % (2386168)Termination phase: Saturation
% 20.63/3.27 % (2386168)Time elapsed: 0.506 s
% 20.63/3.27 % (2386168)Peak memory usage: 19 MB
% 20.63/3.27 % (2386168)Instructions burned: 870 (million)
% 20.63/3.27 % (2386170)ott+10_1_sil=32000:tgt=ground:random_seed=848288733:i=5114:av=off_2978 on theBenchmark for (2978ds/5114Mi)
% 20.63/3.27 % (2386166)Instruction limit reached!
% 20.63/3.27 % (2386166)------------------------------
% 20.63/3.27 % (2386166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386166)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386166)Termination reason: Instruction limit
% 20.63/3.27 % (2386166)Termination phase: Finite model building preprocessing
% 20.63/3.27 % (2386166)Time elapsed: 0.575 s
% 20.63/3.27 % (2386166)Peak memory usage: 40 MB
% 20.63/3.27 % (2386166)Instructions burned: 2177 (million)
% 20.63/3.27 % (2386172)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2634339102:i=54282_2978 on theBenchmark for (2978ds/54282Mi)
% 20.63/3.27 % TRYING [1]
% 20.63/3.27 % TRYING [2]
% 20.63/3.27 % TRYING [3]
% 20.63/3.27 % (2386170) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2386115-2386170"...
% 20.63/3.27 % (2386170)...printing done.
% 20.63/3.27 % (2386170)Refutation found. Thanks to Tanya!
% 20.63/3.27 % SZS status Theorem for theBenchmark
% 20.63/3.27 % SZS output start Proof for theBenchmark
% See solution above
% 20.63/3.27 % (2386170)------------------------------
% 20.63/3.27 % (2386170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.63/3.27 % (2386170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.63/3.27 % (2386170)CaDiCaL version: 2.1.3
% 20.63/3.27 % (2386170)Termination reason: Refutation
% 20.63/3.27 % (2386170)Time elapsed: 0.778 s
% 20.63/3.27 % (2386170)Peak memory usage: 23 MB
% 20.63/3.27 % (2386170)Instructions burned: 1244 (million)
% 20.63/3.27 % (2386115)Success in time 3.008 s
% 20.63/3.27 % Vampire exiting
%------------------------------------------------------------------------------