%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN631-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 02:17:46 PM UTC 2026
% Result : Unsatisfiable 6.47s 1.19s
% Output : Refutation 6.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 25
% Syntax : Number of formulae : 80 ( 42 unt; 14 def)
% Number of atoms : 135 ( 24 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 117 ( 62 ~; 53 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 12 con; 0-3 aty)
% Number of variables : 88 ( 0 sgn 88 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0] : p10(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p10_1) ).
fof(f5,negated_conjecture,
! [X0] : p5(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_5) ).
fof(f11,negated_conjecture,
! [X0,X1] : p5(f16(f18(X0,X1)),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_11) ).
fof(f12,negated_conjecture,
p23(f13(c27,f14(c28)),f11(f15(c24))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p23_12) ).
fof(f13,negated_conjecture,
~ p23(f13(f16(c27),f14(c28)),f11(c24)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p23_13) ).
fof(f18,negated_conjecture,
! [X0,X1] :
( p5(f16(X0),f16(X1))
| ~ p5(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_18) ).
fof(f25,negated_conjecture,
! [X2,X0,X1] :
( ~ p5(X2,X1)
| ~ p5(X2,X0)
| p5(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_25) ).
fof(f29,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p23(X2,X3)
| ~ p12(X2,X0)
| p23(X0,X1)
| ~ p10(X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p23_29) ).
fof(f32,negated_conjecture,
! [X2,X3,X0,X1] :
( p12(f13(X0,X1),f13(X2,X3))
| ~ p5(X0,X2)
| ~ p5(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p12_32) ).
fof(f34,negated_conjecture,
! [X2,X0,X1] :
( p5(X0,f18(f20(c29),f19(X1,X0,X2)))
| ~ p23(f13(X0,X2),f11(f15(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_34) ).
fof(f35,negated_conjecture,
! [X2,X0,X1] :
( p23(f13(f19(X0,X1,X2),X2),f11(X0))
| ~ p23(f13(X1,X2),f11(f15(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p23_35) ).
fof(f42,definition,
! [X0,X1] : sF1(X0,X1) = f16(f18(X0,X1)),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f43,plain,
! [X0,X1] : f16(f18(X0,X1)) = sF1(X0,X1),
inference(reorient_equations,[],[f42]) ).
fof(f44,plain,
! [X0,X1] : p5(sF1(X0,X1),X1),
inference(definition_folding,[],[f11,f43]) ).
fof(f45,definition,
sF2 = f14(c28),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f46,plain,
f14(c28) = sF2,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF3 = f13(c27,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f48,plain,
f13(c27,sF2) = sF3,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF4 = f15(c24),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f50,plain,
f15(c24) = sF4,
inference(reorient_equations,[],[f49]) ).
fof(f51,definition,
sF5 = f11(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f52,plain,
f11(sF4) = sF5,
inference(reorient_equations,[],[f51]) ).
fof(f53,plain,
p23(sF3,sF5),
inference(definition_folding,[],[f12,f52,f50,f48,f46]) ).
fof(f54,definition,
sF6 = f16(c27),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f55,plain,
f16(c27) = sF6,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF7 = f13(sF6,sF2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f57,plain,
f13(sF6,sF2) = sF7,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF8 = f11(c24),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f59,plain,
f11(c24) = sF8,
inference(reorient_equations,[],[f58]) ).
fof(f60,plain,
~ p23(sF7,sF8),
inference(definition_folding,[],[f13,f59,f57,f46,f55]) ).
fof(f61,definition,
sF9 = f20(c29),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f62,plain,
f20(c29) = sF9,
inference(reorient_equations,[],[f61]) ).
fof(f63,definition,
! [X2,X0,X1] : sF10(X1,X0,X2) = f18(sF9,f19(X1,X0,X2)),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f64,plain,
! [X2,X0,X1] : f18(sF9,f19(X1,X0,X2)) = sF10(X1,X0,X2),
inference(reorient_equations,[],[f63]) ).
fof(f65,definition,
! [X1] : sF11(X1) = f11(f15(X1)),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f66,plain,
! [X1] : f11(f15(X1)) = sF11(X1),
inference(reorient_equations,[],[f65]) ).
fof(f67,plain,
! [X2,X0,X1] :
( ~ p23(f13(X0,X2),sF11(X1))
| p5(X0,sF10(X1,X0,X2)) ),
inference(definition_folding,[],[f34,f66,f64,f62]) ).
fof(f68,definition,
! [X2,X0,X1] : sF12(X0,X1,X2) = f13(f19(X0,X1,X2),X2),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f69,plain,
! [X2,X0,X1] : f13(f19(X0,X1,X2),X2) = sF12(X0,X1,X2),
inference(reorient_equations,[],[f68]) ).
fof(f70,plain,
! [X2,X0,X1] :
( p23(sF12(X0,X1,X2),f11(X0))
| ~ p23(f13(X1,X2),sF11(X0)) ),
inference(definition_folding,[],[f35,f66,f69]) ).
fof(f90,plain,
! [X0,X1] :
( ~ p5(X0,X1)
| p5(X1,X0) ),
inference(resolution,[],[f25,f5]) ).
fof(f92,plain,
! [X2,X0,X1] :
( ~ p5(sF1(X0,X1),X2)
| p5(X2,X1) ),
inference(resolution,[],[f25,f44]) ).
fof(f97,plain,
! [X2,X0,X1] :
( ~ p5(f16(f18(X0,X1)),X2)
| p5(X2,X1) ),
inference(forward_demodulation,[],[f92,f43]) ).
fof(f214,plain,
! [X0] :
( p5(f16(X0),sF6)
| ~ p5(X0,c27) ),
inference(superposition,[],[f18,f55]) ).
fof(f218,plain,
! [X0,X1] :
( p23(sF12(c24,X0,X1),sF8)
| ~ p23(f13(X0,X1),sF11(c24)) ),
inference(superposition,[],[f70,f59]) ).
fof(f219,plain,
! [X0,X1] :
( p23(f13(f19(c24,X0,X1),X1),sF8)
| ~ p23(f13(X0,X1),sF11(c24)) ),
inference(forward_demodulation,[],[f218,f69]) ).
fof(f220,plain,
! [X0,X1] :
( ~ p23(f13(X0,X1),f11(f15(c24)))
| p23(f13(f19(c24,X0,X1),X1),sF8) ),
inference(forward_demodulation,[],[f219,f66]) ).
fof(f221,plain,
! [X0,X1] :
( ~ p23(f13(X0,X1),f11(sF4))
| p23(f13(f19(c24,X0,X1),X1),sF8) ),
inference(forward_demodulation,[],[f220,f50]) ).
fof(f222,plain,
! [X0,X1] :
( p23(f13(f19(c24,X0,X1),X1),sF8)
| ~ p23(f13(X0,X1),sF5) ),
inference(forward_demodulation,[],[f221,f52]) ).
fof(f243,plain,
! [X0] :
( ~ p23(sF3,sF11(X0))
| p5(c27,sF10(X0,c27,sF2)) ),
inference(superposition,[],[f67,f48]) ).
fof(f244,plain,
! [X0] :
( ~ p23(sF3,f11(f15(X0)))
| p5(c27,sF10(X0,c27,sF2)) ),
inference(forward_demodulation,[],[f243,f66]) ).
fof(f245,plain,
! [X0] :
( ~ p23(sF3,f11(f15(X0)))
| p5(c27,f18(sF9,f19(X0,c27,sF2))) ),
inference(forward_demodulation,[],[f244,f64]) ).
fof(f250,plain,
! [X0,X1] :
( p12(f13(X0,X1),sF7)
| ~ p5(X0,sF6)
| ~ p5(X1,sF2) ),
inference(superposition,[],[f32,f57]) ).
fof(f312,plain,
! [X0,X1] :
( ~ p5(f18(X1,X0),c27)
| p5(sF6,X0) ),
inference(resolution,[],[f97,f214]) ).
fof(f443,plain,
! [X2,X3,X0,X1] :
( ~ p12(f13(f19(c24,X0,X1),X1),X2)
| ~ p23(f13(X0,X1),sF5)
| p23(X2,X3)
| ~ p10(sF8,X3) ),
inference(resolution,[],[f222,f29]) ).
fof(f451,plain,
( ~ p23(sF3,f11(sF4))
| p5(c27,f18(sF9,f19(c24,c27,sF2))) ),
inference(superposition,[],[f245,f50]) ).
fof(f452,plain,
( ~ p23(sF3,sF5)
| p5(c27,f18(sF9,f19(c24,c27,sF2))) ),
inference(forward_demodulation,[],[f451,f52]) ).
fof(f453,plain,
p5(c27,f18(sF9,f19(c24,c27,sF2))),
inference(forward_subsumption_resolution,[],[f452,f53]) ).
fof(f458,plain,
p5(f18(sF9,f19(c24,c27,sF2)),c27),
inference(resolution,[],[f453,f90]) ).
fof(f527,plain,
p5(sF6,f19(c24,c27,sF2)),
inference(resolution,[],[f458,f312]) ).
fof(f544,plain,
p5(f19(c24,c27,sF2),sF6),
inference(resolution,[],[f527,f90]) ).
fof(f1835,plain,
! [X2,X0,X1] :
( ~ p23(f13(X0,X1),sF5)
| p23(sF7,X2)
| ~ p10(sF8,X2)
| ~ p5(f19(c24,X0,X1),sF6)
| ~ p5(X1,sF2) ),
inference(resolution,[],[f443,f250]) ).
fof(f1838,definition,
( spl16_28
<=> ! [X2] :
( p23(sF7,X2)
| ~ p10(sF8,X2) ) ),
introduced(definition,[new_symbols(definition,[spl16_28])],[avatar_definition]) ).
fof(f1839,plain,
( ! [X2] :
( ~ p10(sF8,X2)
| p23(sF7,X2) )
| ~ spl16_28 ),
inference(avatar_component_clause,[],[f1838]) ).
fof(f1841,definition,
( spl16_29
<=> ! [X0,X1] :
( ~ p23(f13(X0,X1),sF5)
| ~ p5(X1,sF2)
| ~ p5(f19(c24,X0,X1),sF6) ) ),
introduced(definition,[new_symbols(definition,[spl16_29])],[avatar_definition]) ).
fof(f1842,plain,
( ! [X0,X1] :
( ~ p5(f19(c24,X0,X1),sF6)
| ~ p5(X1,sF2)
| ~ p23(f13(X0,X1),sF5) )
| ~ spl16_29 ),
inference(avatar_component_clause,[],[f1841]) ).
fof(f1843,plain,
( spl16_28
| spl16_29 ),
inference(avatar_split_clause,[],[f1835,f1841,f1838]) ).
fof(f1859,plain,
( p23(sF7,sF8)
| ~ spl16_28 ),
inference(resolution,[],[f1839,f1]) ).
fof(f1860,plain,
( $false
| ~ spl16_28 ),
inference(forward_subsumption_resolution,[],[f1859,f60]) ).
fof(f1861,plain,
~ spl16_28,
inference(avatar_contradiction_clause,[],[f1860]) ).
fof(f14612,plain,
( ~ p5(sF2,sF2)
| ~ p23(f13(c27,sF2),sF5)
| ~ spl16_29 ),
inference(resolution,[],[f1842,f544]) ).
fof(f14613,plain,
( ~ p23(f13(c27,sF2),sF5)
| ~ spl16_29 ),
inference(forward_subsumption_resolution,[],[f14612,f5]) ).
fof(f14614,plain,
( ~ p23(sF3,sF5)
| ~ spl16_29 ),
inference(forward_demodulation,[],[f14613,f48]) ).
fof(f14615,plain,
( $false
| ~ spl16_29 ),
inference(forward_subsumption_resolution,[],[f14614,f53]) ).
fof(f14616,plain,
~ spl16_29,
inference(avatar_contradiction_clause,[],[f14615]) ).
cnf(s24,plain,
( spl16_28
| spl16_29 ),
inference(sat_conversion,[],[f1843]) ).
cnf(s28,plain,
~ spl16_28,
inference(sat_conversion,[],[f1861]) ).
cnf(s86,plain,
~ spl16_29,
inference(sat_conversion,[],[f14616]) ).
cnf(s92,plain,
$false,
inference(rat,[],[s24,s86,s28]) ).
fof(f14617,plain,
$false,
inference(avatar_sat_refutation,[],[s92]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN631-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.16 % Computer : n007.cluster.edu
% 0.10/0.16 % Model : x86_64 x86_64
% 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16 % Memory : 8046.5625MB
% 0.10/0.16 % OS : Linux 6.8.0-71-generic
% 0.10/0.16 % CPULimit : 300
% 0.10/0.16 % WCLimit : 300
% 0.10/0.16 % DateTime : Mon Sep 28 16:35:55 UTC 2026
% 0.10/0.16 % CPUTime :
% 0.10/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 Running first-order model finding
% 0.10/0.19 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
% 6.47/1.18 % (2540805)Will run a generic schedule for satisfiability detection.
% 6.47/1.18 % (2540812)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4088846241:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.47/1.18 % (2540811)% WARNING: option uhcvi not known.
% 6.47/1.18 % (2540813)dis+10_1_sil=32000:sp=arity:random_seed=2279409390:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.47/1.18 % (2540810)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4007983395_2999 on theBenchmark for (2999ds/0Mi)
% 6.47/1.18 % (2540811)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=629253092:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.47/1.18 % (2540815)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1334698384:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.47/1.18 % (2540814)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=899276539:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.47/1.18 % (2540816)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2418823123:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.47/1.18 % TRYING [1]
% 6.47/1.18 % TRYING [2]
% 6.47/1.18 % TRYING [3]
% 6.47/1.18 % TRYING [4]
% 6.47/1.18 % (2540814)Instruction limit reached!
% 6.47/1.18 % (2540814)------------------------------
% 6.47/1.18 % (2540814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540814)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540814)Termination reason: Instruction limit
% 6.47/1.18 % (2540814)Termination phase: Saturation
% 6.47/1.18 % (2540814)Time elapsed: 0.058 s
% 6.47/1.18 % (2540814)Peak memory usage: 11 MB
% 6.47/1.18 % (2540814)Instructions burned: 117 (million)
% 6.47/1.18 % (2540813)Instruction limit reached!
% 6.47/1.18 % (2540813)------------------------------
% 6.47/1.18 % (2540813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540813)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540813)Termination reason: Instruction limit
% 6.47/1.18 % (2540813)Termination phase: Saturation
% 6.47/1.18 % (2540813)Time elapsed: 0.061 s
% 6.47/1.18 % (2540813)Peak memory usage: 12 MB
% 6.47/1.18 % (2540813)Instructions burned: 105 (million)
% 6.47/1.18 % TRYING [5]
% 6.47/1.18 % (2540815)Instruction limit reached!
% 6.47/1.18 % (2540815)------------------------------
% 6.47/1.18 % (2540815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540815)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540815)Termination reason: Instruction limit
% 6.47/1.18 % (2540815)Termination phase: Saturation
% 6.47/1.18 % (2540815)Time elapsed: 0.079 s
% 6.47/1.18 % (2540815)Peak memory usage: 13 MB
% 6.47/1.18 % (2540815)Instructions burned: 132 (million)
% 6.47/1.18 % (2540825)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=438926213:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.47/1.18 % (2540824)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3029927058:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.47/1.18 % TRYING [1]
% 6.47/1.18 % TRYING [2]
% 6.47/1.18 % TRYING [3]
% 6.47/1.18 % (2540816)Instruction limit reached!
% 6.47/1.18 % (2540816)------------------------------
% 6.47/1.18 % (2540816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540816)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540816)Termination reason: Instruction limit
% 6.47/1.18 % (2540816)Termination phase: Saturation
% 6.47/1.18 % (2540816)Time elapsed: 0.092 s
% 6.47/1.18 % (2540816)Peak memory usage: 13 MB
% 6.47/1.18 % (2540816)Instructions burned: 160 (million)
% 6.47/1.18 % TRYING [4]
% 6.47/1.18 % (2540826)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=3213973382:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.47/1.18 % (2540829)ott-21_1_sil=16000:fs=off:random_seed=3268749147:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.47/1.18 % TRYING [5]
% 6.47/1.18 % (2540825)Instruction limit reached!
% 6.47/1.18 % (2540825)------------------------------
% 6.47/1.18 % (2540825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540825)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540825)Termination reason: Instruction limit
% 6.47/1.18 % (2540825)Termination phase: Saturation
% 6.47/1.18 % (2540825)Time elapsed: 0.078 s
% 6.47/1.18 % (2540825)Peak memory usage: 14 MB
% 6.47/1.18 % (2540825)Instructions burned: 132 (million)
% 6.47/1.18 % (2540832)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2226771113:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.47/1.18 % (2540829)Instruction limit reached!
% 6.47/1.18 % (2540829)------------------------------
% 6.47/1.18 % (2540829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540829)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540829)Termination reason: Instruction limit
% 6.47/1.18 % (2540829)Termination phase: Saturation
% 6.47/1.18 % (2540829)Time elapsed: 0.101 s
% 6.47/1.18 % (2540829)Peak memory usage: 12 MB
% 6.47/1.18 % (2540829)Instructions burned: 183 (million)
% 6.47/1.18 % (2540834)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=684841507:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.47/1.18 % TRYING [1]
% 6.47/1.18 % TRYING [2]
% 6.47/1.18 % TRYING [3]
% 6.47/1.18 % TRYING [4]
% 6.47/1.18 % TRYING [6]
% 6.47/1.18 % TRYING [6]
% 6.47/1.18 % TRYING [5]
% 6.47/1.18 % TRYING [6]
% 6.47/1.18 % (2540824)Instruction limit reached!
% 6.47/1.18 % (2540824)------------------------------
% 6.47/1.18 % (2540824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540824)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540824)Termination reason: Instruction limit
% 6.47/1.18 % (2540824)Termination phase: Finite model building SAT solving
% 6.47/1.18 % (2540824)Time elapsed: 0.381 s
% 6.47/1.18 % (2540824)Peak memory usage: 28 MB
% 6.47/1.18 % (2540824)Instructions burned: 714 (million)
% 6.47/1.18 % (2540832)Instruction limit reached!
% 6.47/1.18 % (2540832)------------------------------
% 6.47/1.18 % (2540832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540832)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540832)Termination reason: Instruction limit
% 6.47/1.18 % (2540832)Termination phase: Saturation
% 6.47/1.18 % (2540832)Time elapsed: 0.285 s
% 6.47/1.18 % (2540832)Peak memory usage: 14 MB
% 6.47/1.18 % (2540832)Instructions burned: 478 (million)
% 6.47/1.18 % (2540826)Instruction limit reached!
% 6.47/1.18 % (2540826)------------------------------
% 6.47/1.18 % (2540826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (2540826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (2540826)CaDiCaL version: 2.1.3
% 6.47/1.18 % (2540826)Termination reason: Instruction limit
% 6.47/1.18 % (2540826)Termination phase: Saturation
% 6.47/1.18 % (2540826)Time elapsed: 0.376 s
% 6.47/1.18 % (2540826)Peak memory usage: 17 MB
% 6.47/1.18 % (2540826)Instructions burned: 685 (million)
% 6.47/1.18 % (2540912)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1851104525:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 6.47/1.18 % (2540913)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3480840745:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 6.47/1.19 % (2540917)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=2428090862: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)
% 6.47/1.19 % TRYING [14]
% 6.47/1.19 % (2540834)Instruction limit reached!
% 6.47/1.19 % (2540834)------------------------------
% 6.47/1.19 % (2540834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.19 % (2540834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.19 % (2540834)CaDiCaL version: 2.1.3
% 6.47/1.19 % (2540834)Termination reason: Instruction limit
% 6.47/1.19 % (2540834)Termination phase: Finite model building SAT solving
% 6.47/1.19 % (2540834)Time elapsed: 0.435 s
% 6.47/1.19 % (2540834)Peak memory usage: 20 MB
% 6.47/1.19 % (2540834)Instructions burned: 865 (million)
% 6.47/1.19 % (2540956)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1930640113:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 6.47/1.19 % (2540917)Instruction limit reached!
% 6.47/1.19 % (2540917)------------------------------
% 6.47/1.19 % (2540917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.19 % (2540917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.19 % (2540917)CaDiCaL version: 2.1.3
% 6.47/1.19 % (2540917)Termination reason: Instruction limit
% 6.47/1.19 % (2540917)Termination phase: Saturation
% 6.47/1.19 % (2540917)Time elapsed: 0.301 s
% 6.47/1.19 % (2540917)Peak memory usage: 16 MB
% 6.47/1.19 % (2540917)Instructions burned: 693 (million)
% 6.47/1.19 % (2540987)fmb+10_1_sil=64000:random_seed=3291295152:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 6.47/1.19 % TRYING [1]
% 6.47/1.19 % TRYING [2]
% 6.47/1.19 % TRYING [3]
% 6.47/1.19 % TRYING [4]
% 6.47/1.19 % (2540913)Instruction limit reached!
% 6.47/1.19 % (2540913)------------------------------
% 6.47/1.19 % (2540913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.19 % (2540913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.19 % (2540913)CaDiCaL version: 2.1.3
% 6.47/1.19 % (2540913)Termination reason: Instruction limit
% 6.47/1.19 % (2540913)Termination phase: Finite model building constraint generation
% 6.47/1.19 % (2540913)Time elapsed: 0.381 s
% 6.47/1.19 % (2540913)Peak memory usage: 77 MB
% 6.47/1.19 % (2540913)Instructions burned: 890 (million)
% 6.47/1.19 % TRYING [5]
% 6.47/1.19 % (2540990)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2404203528:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 6.47/1.19 % TRYING [20]
% 6.47/1.19 % (2540912) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2540805-2540912"...
% 6.47/1.19 % (2540912)...printing done.
% 6.47/1.19 % (2540912)Refutation found. Thanks to Tanya!
% 6.47/1.19 % SZS status Unsatisfiable for theBenchmark
% 6.47/1.19 % SZS output start Proof for theBenchmark
% See solution above
% 6.47/1.19 % (2540912)------------------------------
% 6.47/1.19 % (2540912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.19 % (2540912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.19 % (2540912)CaDiCaL version: 2.1.3
% 6.47/1.19 % (2540912)Termination reason: Refutation
% 6.47/1.19 % (2540912)Time elapsed: 0.459 s
% 6.47/1.19 % (2540912)Peak memory usage: 21 MB
% 6.47/1.19 % (2540912)Instructions burned: 724 (million)
% 6.47/1.19 % (2540805)Success in time 0.987 s
% 6.47/1.19 % Vampire exiting
%------------------------------------------------------------------------------