%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ANA009-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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 09:31:16 AM UTC 2026
% Result : Unsatisfiable 11.43s 3.47s
% Output : Refutation 11.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 17
% Syntax : Number of formulae : 42 ( 26 unt; 4 def)
% Number of atoms : 62 ( 14 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 44 ( 24 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-3 aty)
% Number of variables : 27 ( 27 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1414,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_plus(c_uminus(X1,X0),X1,X0) = c_0 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oab__group__add__class_Oaxioms__1_0) ).
fof(f1415,plain,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_0 = c_plus(c_uminus(X1,X0),X1,X0) ),
inference(reorient_equations,[],[f1414]) ).
fof(f1439,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(c_plus(X3,X1,X0),c_plus(X3,X2,X0),X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oadd__le__cancel__left_1) ).
fof(f1477,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_uminus(c_uminus(X1,X0),X0) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Ominus__minus_0) ).
fof(f1495,axiom,
! [X2,X0,X1] :
( c_lessequals(c_uminus(X2,X0),c_uminus(X1,X0),X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_OrderedGroup_Opordered__ab__group__add(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oneg__le__iff__le_1) ).
fof(f2720,axiom,
! [X0] :
( ~ class_Ring__and__Field_Ocomm__ring__1(X0)
| class_OrderedGroup_Oab__group__add(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Ocomm__ring__1_2) ).
fof(f2888,axiom,
! [X0] :
( ~ class_Ring__and__Field_Olordered__ring(X0)
| class_OrderedGroup_Opordered__ab__group__add(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Olordered__ring_2) ).
fof(f2916,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__comm__semiring__strict(X0)
| class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__comm__semiring__strict_17) ).
fof(f2998,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_Ring__and__Field_Ocomm__ring__1(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__idom_0) ).
fof(f3022,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_Ring__and__Field_Oordered__comm__semiring__strict(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__idom_30) ).
fof(f3041,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_Ring__and__Field_Olordered__ring(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__idom_48) ).
fof(f3364,negated_conjecture,
! [X0] : c_lessequals(v_lb(X0),v_f(X0),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f3366,negated_conjecture,
~ c_lessequals(c_0,c_plus(v_f(v_x),c_uminus(v_lb(v_x),t_b),t_b),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f3367,negated_conjecture,
class_Ring__and__Field_Oordered__idom(t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
fof(f3588,definition,
sF0 = v_f(v_x),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f3589,plain,
v_f(v_x) = sF0,
inference(reorient_equations,[],[f3588]) ).
fof(f3590,definition,
sF1 = v_lb(v_x),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f3591,plain,
v_lb(v_x) = sF1,
inference(reorient_equations,[],[f3590]) ).
fof(f3592,definition,
sF2 = c_uminus(sF1,t_b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f3593,plain,
c_uminus(sF1,t_b) = sF2,
inference(reorient_equations,[],[f3592]) ).
fof(f3594,definition,
sF3 = c_plus(sF0,sF2,t_b),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f3595,plain,
c_plus(sF0,sF2,t_b) = sF3,
inference(reorient_equations,[],[f3594]) ).
fof(f3596,plain,
~ c_lessequals(c_0,sF3,t_b),
inference(definition_folding,[],[f3366,f3595,f3593,f3591,f3589]) ).
fof(f4358,plain,
class_Ring__and__Field_Ocomm__ring__1(t_b),
inference(resolution,[],[f2998,f3367]) ).
fof(f4372,plain,
class_OrderedGroup_Oab__group__add(t_b),
inference(resolution,[],[f4358,f2720]) ).
fof(f4526,plain,
class_Ring__and__Field_Oordered__comm__semiring__strict(t_b),
inference(resolution,[],[f3022,f3367]) ).
fof(f4537,plain,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(t_b),
inference(resolution,[],[f4526,f2916]) ).
fof(f4682,plain,
class_Ring__and__Field_Olordered__ring(t_b),
inference(resolution,[],[f3041,f3367]) ).
fof(f4696,plain,
class_OrderedGroup_Opordered__ab__group__add(t_b),
inference(resolution,[],[f4682,f2888]) ).
fof(f5603,plain,
c_lessequals(v_lb(v_x),sF0,t_b),
inference(superposition,[],[f3364,f3589]) ).
fof(f5604,plain,
c_lessequals(sF1,sF0,t_b),
inference(forward_demodulation,[],[f5603,f3591]) ).
fof(f6473,plain,
! [X0] : c_uminus(c_uminus(X0,t_b),t_b) = X0,
inference(resolution,[],[f1477,f4372]) ).
fof(f6850,plain,
! [X0] : c_0 = c_plus(c_uminus(X0,t_b),X0,t_b),
inference(resolution,[],[f1415,f4372]) ).
fof(f6854,plain,
! [X0] : c_0 = c_plus(X0,c_uminus(X0,t_b),t_b),
inference(superposition,[],[f6850,f6473]) ).
fof(f14605,plain,
! [X0] :
( c_lessequals(c_uminus(X0,t_b),sF2,t_b)
| ~ c_lessequals(sF1,X0,t_b)
| ~ class_OrderedGroup_Opordered__ab__group__add(t_b) ),
inference(superposition,[],[f1495,f3593]) ).
fof(f14609,plain,
! [X0] :
( c_lessequals(c_uminus(X0,t_b),sF2,t_b)
| ~ c_lessequals(sF1,X0,t_b) ),
inference(forward_subsumption_resolution,[],[f14605,f4696]) ).
fof(f19680,plain,
! [X0] :
( c_lessequals(c_plus(sF0,X0,t_b),sF3,t_b)
| ~ c_lessequals(X0,sF2,t_b)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(t_b) ),
inference(superposition,[],[f1439,f3595]) ).
fof(f19686,plain,
! [X0] :
( c_lessequals(c_plus(sF0,X0,t_b),sF3,t_b)
| ~ c_lessequals(X0,sF2,t_b) ),
inference(forward_subsumption_resolution,[],[f19680,f4537]) ).
fof(f21951,plain,
( c_lessequals(c_0,sF3,t_b)
| ~ c_lessequals(c_uminus(sF0,t_b),sF2,t_b) ),
inference(superposition,[],[f19686,f6854]) ).
fof(f21952,plain,
~ c_lessequals(c_uminus(sF0,t_b),sF2,t_b),
inference(forward_subsumption_resolution,[],[f21951,f3596]) ).
fof(f21976,plain,
~ c_lessequals(sF1,sF0,t_b),
inference(resolution,[],[f21952,f14609]) ).
fof(f21978,plain,
$false,
inference(forward_subsumption_resolution,[],[f21976,f5604]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA009-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n020.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 20:29:15 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.47/2.06 % (499877)Will run a generic schedule for satisfiability detection.
% 12.47/2.06 % (499884)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1392496248:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 12.47/2.06 % (499883)% WARNING: option uhcvi not known.
% 12.47/2.06 % (499882)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3021504385_2999 on theBenchmark for (2999ds/0Mi)
% 12.47/2.06 % (499883)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3719276669:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 12.47/2.06 % (499885)dis+10_1_sil=32000:sp=arity:random_seed=3510427371:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 12.47/2.06 % (499886)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2551940882:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 12.47/2.06 % (499888)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3359420193:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 12.47/2.06 % (499887)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4036921045:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 12.47/2.06 % (499885)Instruction limit reached!
% 12.47/2.06 % (499885)------------------------------
% 12.47/2.06 % (499885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.47/2.06 % (499885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.06 % (499885)CaDiCaL version: 2.1.3
% 12.47/2.06 % (499885)Termination reason: Instruction limit
% 12.47/2.06 % (499885)Termination phase: Saturation
% 12.47/2.06 % (499885)Time elapsed: 0.057 s
% 12.47/2.06 % (499885)Peak memory usage: 15 MB
% 12.47/2.06 % (499885)Instructions burned: 104 (million)
% 12.47/2.06 % (499886)Instruction limit reached!
% 12.47/2.06 % (499886)------------------------------
% 12.47/2.06 % (499886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.47/2.06 % (499886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.06 % (499886)CaDiCaL version: 2.1.3
% 12.47/2.06 % (499886)Termination reason: Instruction limit
% 12.47/2.06 % (499886)Termination phase: Saturation
% 12.47/2.06 % (499886)Time elapsed: 0.062 s
% 12.47/2.06 % (499886)Peak memory usage: 15 MB
% 12.47/2.06 % (499886)Instructions burned: 117 (million)
% 12.47/2.06 % (499896)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1796742739:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 12.47/2.06 % (499897)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1591523210:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 12.47/2.06 % (499887)Instruction limit reached!
% 12.47/2.06 % (499887)------------------------------
% 12.47/2.06 % (499887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.47/2.06 % (499887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.06 % (499887)CaDiCaL version: 2.1.3
% 12.47/2.06 % (499887)Termination reason: Instruction limit
% 12.47/2.06 % (499887)Termination phase: Saturation
% 12.47/2.06 % (499887)Time elapsed: 0.087 s
% 12.47/2.06 % (499887)Peak memory usage: 16 MB
% 12.47/2.06 % (499887)Instructions burned: 132 (million)
% 12.47/2.06 % (499888)Instruction limit reached!
% 12.47/2.06 % (499888)------------------------------
% 12.47/2.06 % (499888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.47/2.06 % (499888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.06 % (499888)CaDiCaL version: 2.1.3
% 12.47/2.06 % (499888)Termination reason: Instruction limit
% 12.47/2.06 % (499888)Termination phase: Saturation
% 12.47/2.06 % (499888)Time elapsed: 0.091 s
% 12.47/2.06 % (499888)Peak memory usage: 16 MB
% 12.47/2.06 % (499888)Instructions burned: 159 (million)
% 12.47/2.06 % (499900)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=43585646:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 12.47/2.06 % (499901)ott-21_1_sil=16000:fs=off:random_seed=1350104408:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 12.47/2.06 % (499897)Instruction limit reached!
% 12.47/2.06 % (499897)------------------------------
% 12.47/2.06 % (499897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.47/2.06 % (499897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.47/2.06 % (499897)CaDiCaL version: 2.1.3
% 12.47/2.06 % (499897)Termination reason: Instruction limit
% 11.43/3.46 % (499897)Termination phase: Saturation
% 11.43/3.46 % (499897)Time elapsed: 0.073 s
% 11.43/3.46 % (499897)Peak memory usage: 16 MB
% 11.43/3.46 % (499897)Instructions burned: 131 (million)
% 11.43/3.46 % (499904)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1481216194:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 11.43/3.46 % (499901)Instruction limit reached!
% 11.43/3.46 % (499901)------------------------------
% 11.43/3.46 % (499901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499901)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499901)Termination reason: Instruction limit
% 11.43/3.46 % (499901)Termination phase: Saturation
% 11.43/3.46 % (499901)Time elapsed: 0.097 s
% 11.43/3.46 % (499901)Peak memory usage: 16 MB
% 11.43/3.46 % (499901)Instructions burned: 180 (million)
% 11.43/3.46 % (499906)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=673229586:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 11.43/3.46 % TRYING [1]
% 11.43/3.46 % TRYING [2]
% 11.43/3.46 % TRYING [1]
% 11.43/3.46 % TRYING [2]
% 11.43/3.46 % (499896)Instruction limit reached!
% 11.43/3.46 % (499896)------------------------------
% 11.43/3.46 % (499896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499896)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499896)Termination reason: Instruction limit
% 11.43/3.46 % (499896)Termination phase: Finite model building constraint generation
% 11.43/3.46 % (499896)Time elapsed: 0.334 s
% 11.43/3.46 % (499896)Peak memory usage: 26 MB
% 11.43/3.46 % (499896)Instructions burned: 715 (million)
% 11.43/3.46 % (499908)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2610745153:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 11.43/3.46 % (499904)Instruction limit reached!
% 11.43/3.46 % (499904)------------------------------
% 11.43/3.46 % (499904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499904)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499904)Termination reason: Instruction limit
% 11.43/3.46 % (499904)Termination phase: Saturation
% 11.43/3.46 % (499904)Time elapsed: 0.297 s
% 11.43/3.46 % (499904)Peak memory usage: 17 MB
% 11.43/3.46 % (499904)Instructions burned: 477 (million)
% 11.43/3.46 % (499900)Instruction limit reached!
% 11.43/3.46 % (499900)------------------------------
% 11.43/3.46 % (499900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499900)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499900)Termination reason: Instruction limit
% 11.43/3.46 % (499900)Termination phase: Saturation
% 11.43/3.46 % (499900)Time elapsed: 0.385 s
% 11.43/3.46 % (499900)Peak memory usage: 19 MB
% 11.43/3.46 % (499900)Instructions burned: 684 (million)
% 11.43/3.46 % (499910)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1498832054:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 11.43/3.46 % (499912)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=38485647: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)
% 11.43/3.46 % TRYING [1]
% 11.43/3.46 % (499906)Instruction limit reached!
% 11.43/3.46 % (499906)------------------------------
% 11.43/3.46 % (499906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499906)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499906)Termination reason: Instruction limit
% 11.43/3.46 % (499906)Termination phase: Finite model building constraint generation
% 11.43/3.46 % (499906)Time elapsed: 0.428 s
% 11.43/3.46 % (499906)Peak memory usage: 49 MB
% 11.43/3.46 % (499906)Instructions burned: 865 (million)
% 11.43/3.46 % (499914)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3231180306:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 11.43/3.46 % (499910)Cannot represent all propositional literals internally
% 11.43/3.46 % (499910)Refutation not found, incomplete strategy
% 11.43/3.46 % (499910)------------------------------
% 11.43/3.46 % (499910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499910)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499910)Termination reason: Refutation not found, incomplete strategy
% 11.43/3.46 % (499910)Time elapsed: 0.282 s
% 11.43/3.46 % (499910)Peak memory usage: 23 MB
% 11.43/3.46 % (499910)Instructions burned: 574 (million)
% 11.43/3.46 % (499910)------------------------------
% 11.43/3.46 % (499910)------------------------------
% 11.43/3.46 % (499916)fmb+10_1_sil=64000:random_seed=1311569408:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 11.43/3.46 % (499912)Instruction limit reached!
% 11.43/3.46 % (499912)------------------------------
% 11.43/3.46 % (499912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499912)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499912)Termination reason: Instruction limit
% 11.43/3.46 % (499912)Termination phase: Saturation
% 11.43/3.46 % (499912)Time elapsed: 0.371 s
% 11.43/3.46 % (499912)Peak memory usage: 21 MB
% 11.43/3.46 % (499912)Instructions burned: 694 (million)
% 11.43/3.46 % (499918)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1018258943:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 11.43/3.46 % TRYING [1]
% 11.43/3.46 % (499914)Instruction limit reached!
% 11.43/3.46 % (499914)------------------------------
% 11.43/3.46 % (499914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499914)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499914)Termination reason: Instruction limit
% 11.43/3.46 % (499914)Termination phase: Saturation
% 11.43/3.46 % (499914)Time elapsed: 0.436 s
% 11.43/3.46 % (499914)Peak memory usage: 21 MB
% 11.43/3.46 % (499914)Instructions burned: 880 (million)
% 11.43/3.46 % (499920)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2726429030:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 11.43/3.46 % (499908)Instruction limit reached!
% 11.43/3.46 % (499908)------------------------------
% 11.43/3.46 % (499908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499908)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499908)Termination reason: Instruction limit
% 11.43/3.46 % (499908)Termination phase: Saturation
% 11.43/3.46 % (499908)Time elapsed: 0.719 s
% 11.43/3.46 % (499908)Peak memory usage: 26 MB
% 11.43/3.46 % (499908)Instructions burned: 1180 (million)
% 11.43/3.46 % (499922)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1851341969:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 11.43/3.46 % (499918)Cannot represent all propositional literals internally
% 11.43/3.46 % (499918)Refutation not found, incomplete strategy
% 11.43/3.46 % (499918)------------------------------
% 11.43/3.46 % (499918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499918)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499918)Termination reason: Refutation not found, incomplete strategy
% 11.43/3.46 % (499918)Time elapsed: 0.286 s
% 11.43/3.46 % (499918)Peak memory usage: 23 MB
% 11.43/3.46 % (499918)Instructions burned: 571 (million)
% 11.43/3.46 % (499918)------------------------------
% 11.43/3.46 % (499918)------------------------------
% 11.43/3.46 % (499924)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=415318976:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 11.43/3.46 % (499920)Cannot represent all propositional literals internally
% 11.43/3.46 % (499920)Refutation not found, incomplete strategy
% 11.43/3.46 % (499920)------------------------------
% 11.43/3.46 % (499920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.46 % (499920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.46 % (499920)CaDiCaL version: 2.1.3
% 11.43/3.46 % (499920)Termination reason: Refutation not found, incomplete strategy
% 11.43/3.46 % (499920)Time elapsed: 0.282 s
% 11.43/3.46 % (499920)Peak memory usage: 23 MB
% 11.43/3.46 % (499920)Instructions burned: 571 (million)
% 11.43/3.46 % (499920)------------------------------
% 11.43/3.46 % (499920)------------------------------
% 11.43/3.46 % (499926)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2588824115:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 11.43/3.46 % TRYING [2]
% 11.43/3.46 % (499926)Cannot represent all propositional literals internally
% 11.43/3.47 % (499926)Refutation not found, incomplete strategy
% 11.43/3.47 % (499926)------------------------------
% 11.43/3.47 % (499926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.47 % (499926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.47 % (499926)CaDiCaL version: 2.1.3
% 11.43/3.47 % (499926)Termination reason: Refutation not found, incomplete strategy
% 11.43/3.47 % (499926)Time elapsed: 0.293 s
% 11.43/3.47 % (499926)Peak memory usage: 23 MB
% 11.43/3.47 % (499926)Instructions burned: 592 (million)
% 11.43/3.47 % (499926)------------------------------
% 11.43/3.47 % (499926)------------------------------
% 11.43/3.47 % (499928)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3276438708:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi)
% 11.43/3.47 % (499924)Instruction limit reached!
% 11.43/3.47 % (499924)------------------------------
% 11.43/3.47 % (499924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.47 % (499924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.47 % (499924)CaDiCaL version: 2.1.3
% 11.43/3.47 % (499924)Termination reason: Instruction limit
% 11.43/3.47 % (499924)Termination phase: Saturation
% 11.43/3.47 % (499924)Time elapsed: 0.770 s
% 11.43/3.47 % (499924)Peak memory usage: 33 MB
% 11.43/3.47 % (499924)Instructions burned: 1472 (million)
% 11.43/3.47 % (499930)ott-2_1_sil=16000:newcnf=on:random_seed=553180122:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi)
% 11.43/3.47 % (499930)Instruction limit reached!
% 11.43/3.47 % (499930)------------------------------
% 11.43/3.47 % (499930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.47 % (499930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.47 % (499930)CaDiCaL version: 2.1.3
% 11.43/3.47 % (499930)Termination reason: Instruction limit
% 11.43/3.47 % (499930)Termination phase: Saturation
% 11.43/3.47 % (499930)Time elapsed: 0.512 s
% 11.43/3.47 % (499930)Peak memory usage: 21 MB
% 11.43/3.47 % (499930)Instructions burned: 870 (million)
% 11.43/3.47 % (499932)ott+10_1_sil=32000:tgt=ground:random_seed=957018144:i=5114:av=off_2973 on theBenchmark for (2973ds/5114Mi)
% 11.43/3.47 % (499928)Instruction limit reached!
% 11.43/3.47 % (499928)------------------------------
% 11.43/3.47 % (499928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.47 % (499928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.47 % (499928)CaDiCaL version: 2.1.3
% 11.43/3.47 % (499928)Termination reason: Instruction limit
% 11.43/3.47 % (499928)Termination phase: Finite model building preprocessing
% 11.43/3.47 % (499928)Time elapsed: 1.090 s
% 11.43/3.47 % (499928)Peak memory usage: 41 MB
% 11.43/3.47 % (499928)Instructions burned: 2176 (million)
% 11.43/3.47 % (499934)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3409504025:i=54282_2970 on theBenchmark for (2970ds/54282Mi)
% 11.43/3.47 % (499932) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-499877-499932"...
% 11.43/3.47 % (499932)...printing done.
% 11.43/3.47 % (499932)Refutation found. Thanks to Tanya!
% 11.43/3.47 % SZS status Unsatisfiable for theBenchmark
% 11.43/3.47 % SZS output start Proof for theBenchmark
% See solution above
% 11.43/3.47 % (499932)------------------------------
% 11.43/3.47 % (499932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.43/3.47 % (499932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.43/3.47 % (499932)CaDiCaL version: 2.1.3
% 11.43/3.47 % (499932)Termination reason: Refutation
% 11.43/3.47 % (499932)Time elapsed: 0.500 s
% 11.43/3.47 % (499932)Peak memory usage: 22 MB
% 11.43/3.47 % (499932)Instructions burned: 780 (million)
% 11.43/3.47 % (499877)Success in time 3.246 s
% 11.43/3.47 % Vampire exiting
%------------------------------------------------------------------------------