%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE170+1.006 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 11:40:33 AM UTC 2026
% Result : Theorem 13.22s 2.99s
% Output : Refutation 15.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 13
% Syntax : Number of formulae : 75 ( 40 unt; 1 def)
% Number of atoms : 115 ( 25 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 86 ( 46 ~; 36 |; 1 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 131 ( 0 sgn 131 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_associativity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_distributivity) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_distributivity) ).
fof(f12,axiom,
! [X0,X1] :
( leq(X0,X1)
<=> addition(X0,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',order) ).
fof(f13,axiom,
! [X0] : leq(addition(one,multiplication(X0,star(X0))),star(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',star_unfold_right) ).
fof(f14,axiom,
! [X0] : leq(addition(one,multiplication(star(X0),X0)),star(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',star_unfold_left) ).
fof(f15,axiom,
! [X0,X1,X2] :
( leq(addition(multiplication(X0,X1),X2),X1)
=> leq(multiplication(star(X0),X2),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',star_induction_left) ).
fof(f17,conjecture,
leq(multiplication(a,multiplication(a,multiplication(a,multiplication(a,multiplication(a,a))))),star(a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a) ).
fof(f18,negated_conjecture,
~ leq(multiplication(a,multiplication(a,multiplication(a,multiplication(a,multiplication(a,a))))),star(a)),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
~ leq(multiplication(a,multiplication(a,multiplication(a,multiplication(a,multiplication(a,a))))),star(a)),
inference(flattening,[],[f18]) ).
fof(f21,plain,
! [X0,X1,X2] :
( leq(multiplication(star(X0),X2),X1)
| ~ leq(addition(multiplication(X0,X1),X2),X1) ),
inference(ennf_transformation,[],[f15]) ).
fof(f22,plain,
! [X0,X1] :
( ( leq(X0,X1)
| addition(X0,X1) != X1 )
& ( addition(X0,X1) = X1
| ~ leq(X0,X1) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f23,plain,
~ leq(multiplication(a,multiplication(a,multiplication(a,multiplication(a,multiplication(a,a))))),star(a)),
inference(cnf_transformation,[],[f19]) ).
fof(f25,plain,
! [X2,X0,X1] :
( ~ leq(addition(multiplication(X0,X1),X2),X1)
| leq(multiplication(star(X0),X2),X1) ),
inference(cnf_transformation,[],[f21]) ).
fof(f26,plain,
! [X0] : leq(addition(one,multiplication(star(X0),X0)),star(X0)),
inference(cnf_transformation,[],[f14]) ).
fof(f27,plain,
! [X0] : leq(addition(one,multiplication(X0,star(X0))),star(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f28,plain,
! [X0,X1] :
( addition(X0,X1) = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f29,plain,
! [X0,X1] :
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f32,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f33,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f36,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f37,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f39,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f40,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f58,plain,
! [X0,X1] :
( addition(X0,X1) = X0
| ~ leq(X1,X0) ),
inference(superposition,[],[f40,f28]) ).
fof(f82,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f39,f37]) ).
fof(f91,plain,
! [X2,X0,X1] :
( addition(X0,addition(X1,X2)) = X2
| ~ leq(addition(X0,X1),X2) ),
inference(superposition,[],[f28,f39]) ).
fof(f108,plain,
! [X0,X1] :
( addition(X0,X1) != addition(X0,X1)
| leq(X0,addition(X0,X1)) ),
inference(superposition,[],[f29,f82]) ).
fof(f112,plain,
! [X0,X1] : leq(X0,addition(X0,X1)),
inference(trivial_inequality_removal,[],[f108]) ).
fof(f127,plain,
! [X2,X0,X1] : leq(multiplication(X0,X2),multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f112,f32]) ).
fof(f128,plain,
! [X2,X0,X1] : leq(addition(X0,X1),addition(X0,addition(X1,X2))),
inference(superposition,[],[f112,f39]) ).
fof(f145,plain,
! [X2,X0,X1] : leq(multiplication(X0,X1),multiplication(X0,addition(X1,X2))),
inference(superposition,[],[f112,f33]) ).
fof(f158,plain,
! [X2,X0,X1] :
( leq(multiplication(X1,X2),multiplication(X1,X0))
| ~ leq(X2,X0) ),
inference(superposition,[],[f145,f28]) ).
fof(f213,plain,
! [X2,X0,X1] :
( ~ leq(addition(X1,X2),X0)
| addition(X1,X0) = X0 ),
inference(superposition,[],[f82,f91]) ).
fof(f214,plain,
! [X2,X0,X1] :
( ~ leq(addition(X1,X2),X0)
| leq(X1,X0) ),
inference(superposition,[],[f112,f91]) ).
fof(f230,plain,
! [X2,X0,X1] :
( leq(multiplication(star(X0),multiplication(X0,X2)),X1)
| ~ leq(multiplication(X0,addition(X1,X2)),X1) ),
inference(superposition,[],[f25,f33]) ).
fof(f241,plain,
! [X2,X0,X1] :
( leq(multiplication(X1,X2),multiplication(X0,X2))
| ~ leq(X1,X0) ),
inference(superposition,[],[f127,f28]) ).
fof(f254,plain,
! [X2,X3,X0,X1] :
( leq(multiplication(X0,multiplication(X1,X2)),multiplication(X3,X2))
| ~ leq(multiplication(X0,X1),X3) ),
inference(superposition,[],[f241,f36]) ).
fof(f278,plain,
! [X2,X0,X1] :
( leq(addition(X1,X2),addition(X1,X0))
| ~ leq(X2,X0) ),
inference(superposition,[],[f128,f28]) ).
fof(f566,plain,
! [X0] : star(X0) = addition(one,star(X0)),
inference(resolution,[],[f213,f26]) ).
fof(f624,plain,
! [X0,X1] : leq(multiplication(X1,one),multiplication(X1,star(X0))),
inference(superposition,[],[f145,f566]) ).
fof(f631,plain,
! [X0,X1] : leq(X1,multiplication(X1,star(X0))),
inference(forward_demodulation,[],[f624,f35]) ).
fof(f661,plain,
! [X2,X0,X1] :
( leq(X1,X2)
| ~ leq(X0,X2)
| ~ leq(X1,X0) ),
inference(superposition,[],[f214,f28]) ).
fof(f663,plain,
! [X2,X0,X1] :
( ~ leq(addition(X0,X1),X2)
| leq(X1,X2) ),
inference(superposition,[],[f214,f40]) ).
fof(f980,plain,
! [X0] : leq(multiplication(X0,star(X0)),star(X0)),
inference(resolution,[],[f663,f27]) ).
fof(f1001,plain,
! [X2,X3,X0,X1] :
( ~ leq(multiplication(X0,addition(X1,X2)),X3)
| leq(multiplication(X0,X2),X3) ),
inference(superposition,[],[f663,f33]) ).
fof(f1927,plain,
! [X2,X3,X0,X1,X4] :
( leq(multiplication(X3,multiplication(X0,multiplication(X1,X2))),multiplication(X4,X2))
| ~ leq(multiplication(X3,multiplication(X0,X1)),X4) ),
inference(superposition,[],[f254,f36]) ).
fof(f1957,plain,
! [X0] :
( ~ leq(multiplication(a,multiplication(a,multiplication(a,multiplication(a,multiplication(a,a))))),X0)
| ~ leq(X0,star(a)) ),
inference(resolution,[],[f661,f23]) ).
fof(f1962,plain,
! [X2,X3,X0,X1] :
( ~ leq(addition(X2,X3),X0)
| ~ leq(X0,X1)
| leq(X3,X1) ),
inference(resolution,[],[f661,f663]) ).
fof(f2053,definition,
( spl0_10
<=> leq(multiplication(a,a),star(a)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f2054,plain,
( leq(multiplication(a,a),star(a))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f2053]) ).
fof(f2055,plain,
( ~ leq(multiplication(a,a),star(a))
| spl0_10 ),
inference(avatar_component_clause,[],[f2053]) ).
fof(f4598,plain,
! [X0] :
( ~ leq(multiplication(X0,multiplication(a,multiplication(a,a))),star(a))
| ~ leq(multiplication(a,multiplication(a,a)),X0) ),
inference(resolution,[],[f1927,f1957]) ).
fof(f4623,plain,
( ~ leq(multiplication(a,multiplication(a,a)),star(a))
| ~ leq(multiplication(a,addition(star(a),multiplication(a,a))),star(a)) ),
inference(resolution,[],[f4598,f230]) ).
fof(f4643,plain,
~ leq(multiplication(a,addition(star(a),multiplication(a,a))),star(a)),
inference(forward_subsumption_resolution,[],[f4623,f1001]) ).
fof(f4647,plain,
( ~ leq(multiplication(a,star(a)),star(a))
| ~ leq(multiplication(a,a),star(a)) ),
inference(superposition,[],[f4643,f58]) ).
fof(f5085,plain,
! [X2,X3,X0,X1] :
( ~ leq(addition(X0,X1),X2)
| leq(X3,X2)
| ~ leq(X3,X1) ),
inference(resolution,[],[f1962,f278]) ).
fof(f5148,plain,
! [X0,X1] :
( ~ leq(X0,multiplication(X1,star(X1)))
| leq(X0,star(X1)) ),
inference(resolution,[],[f5085,f27]) ).
fof(f5192,plain,
! [X0] : leq(X0,star(X0)),
inference(resolution,[],[f5148,f631]) ).
fof(f5202,plain,
! [X0,X1] :
( leq(multiplication(X0,X1),star(X0))
| ~ leq(X1,star(X0)) ),
inference(resolution,[],[f5148,f158]) ).
fof(f5316,plain,
( ~ leq(a,star(a))
| spl0_10 ),
inference(resolution,[],[f5202,f2055]) ).
fof(f5327,plain,
( $false
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f5316,f5192]) ).
fof(f5328,plain,
spl0_10,
inference(avatar_contradiction_clause,[],[f5327]) ).
fof(f5330,plain,
~ leq(multiplication(a,a),star(a)),
inference(forward_subsumption_resolution,[],[f4647,f980]) ).
fof(f5335,plain,
( $false
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f5330,f2054]) ).
fof(f5336,plain,
~ spl0_10,
inference(avatar_contradiction_clause,[],[f5335]) ).
cnf(s10,plain,
spl0_10,
inference(sat_conversion,[],[f5328]) ).
cnf(s12,plain,
~ spl0_10,
inference(sat_conversion,[],[f5336]) ).
cnf(s13,plain,
$false,
inference(rat,[],[s10,s12]) ).
fof(f5337,plain,
$false,
inference(avatar_sat_refutation,[],[s13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE170+1.006 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 % Computer : n009.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Sun Sep 27 13:15:15 UTC 2026
% 0.11/0.42 % CPUTime :
% 0.11/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.45 Running first-order theorem proving
% 0.11/0.45 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.84/2.51 % (2033873)Detected formulas, will run a generic FOF schedule.
% 10.84/2.51 % (2033878)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1997043538:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.84/2.51 % (2033884)dis-21_1_sil=8000:lcm=predicate:random_seed=424199476:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.84/2.51 % (2033879)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1628697057:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.84/2.51 % (2033883)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1763290194:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.84/2.51 % (2033881)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4078842618:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.84/2.51 % (2033882)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3266511764:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.84/2.51 % (2033880)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=850207765:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.84/2.51 % (2033881)Refutation not found, incomplete strategy
% 10.84/2.51 % (2033881)------------------------------
% 10.84/2.51 % (2033881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.51 % (2033881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.51 % (2033881)CaDiCaL version: 2.1.3
% 10.84/2.51 % (2033881)Termination reason: Refutation not found, incomplete strategy
% 10.84/2.51 % (2033881)Time elapsed: 0.001 s
% 10.84/2.51 % (2033881)Peak memory usage: 88 MB
% 10.84/2.51 % (2033884)Refutation not found, incomplete strategy
% 10.84/2.51 % (2033884)------------------------------
% 10.84/2.51 % (2033884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.51 % (2033884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.51 % (2033884)CaDiCaL version: 2.1.3
% 10.84/2.51 % (2033884)Termination reason: Refutation not found, incomplete strategy
% 10.84/2.51 % (2033884)Time elapsed: 0.001 s
% 10.84/2.51 % (2033884)Peak memory usage: 88 MB
% 10.84/2.51 % (2033884)Instructions burned: 1 (million)
% 10.84/2.51 % (2033882)Instruction limit reached!
% 10.84/2.51 % (2033882)------------------------------
% 10.84/2.51 % (2033882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.51 % (2033882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.51 % (2033882)CaDiCaL version: 2.1.3
% 10.84/2.51 % (2033882)Termination reason: Instruction limit
% 10.84/2.51 % (2033882)Termination phase: Saturation
% 10.84/2.51 % (2033882)Time elapsed: 0.068 s
% 10.84/2.51 % (2033882)Peak memory usage: 88 MB
% 10.84/2.51 % (2033882)Instructions burned: 121 (million)
% 10.84/2.51 % (2033883)Instruction limit reached!
% 10.84/2.51 % (2033883)------------------------------
% 10.84/2.51 % (2033883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.51 % (2033883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.51 % (2033883)CaDiCaL version: 2.1.3
% 10.84/2.51 % (2033883)Termination reason: Instruction limit
% 10.84/2.51 % (2033883)Termination phase: Saturation
% 10.84/2.51 % (2033883)Time elapsed: 0.085 s
% 10.84/2.51 % (2033883)Peak memory usage: 90 MB
% 10.84/2.51 % (2033883)Instructions burned: 139 (million)
% 10.84/2.51 % (2033892)lrs+10_1_sil=8000:sp=occurrence:random_seed=937775438:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.84/2.51 % (2033881)------------------------------
% 10.84/2.51 % (2033881)------------------------------
% 10.84/2.51 % (2033884)------------------------------
% 10.84/2.51 % (2033884)------------------------------
% 10.84/2.51 % (2033893)lrs+10_1_sil=32000:urr=on:br=off:random_seed=185475398:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.84/2.51 % (2033893)Instruction limit reached!
% 10.84/2.51 % (2033893)------------------------------
% 10.84/2.51 % (2033893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.51 % (2033893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033893)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033893)Termination reason: Instruction limit
% 13.22/2.99 % (2033893)Termination phase: Saturation
% 13.22/2.99 % (2033893)Time elapsed: 0.082 s
% 13.22/2.99 % (2033893)Peak memory usage: 89 MB
% 13.22/2.99 % (2033893)Instructions burned: 159 (million)
% 13.22/2.99 % (2033897)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=484583172:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 13.22/2.99 % (2033896)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2993520816:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 13.22/2.99 % (2033892)Instruction limit reached!
% 13.22/2.99 % (2033892)------------------------------
% 13.22/2.99 % (2033892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033892)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033892)Termination reason: Instruction limit
% 13.22/2.99 % (2033892)Termination phase: Saturation
% 13.22/2.99 % (2033892)Time elapsed: 0.182 s
% 13.22/2.99 % (2033892)Peak memory usage: 91 MB
% 13.22/2.99 % (2033892)Instructions burned: 285 (million)
% 13.22/2.99 % (2033897)Instruction limit reached!
% 13.22/2.99 % (2033897)------------------------------
% 13.22/2.99 % (2033897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033897)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033897)Termination reason: Instruction limit
% 13.22/2.99 % (2033897)Termination phase: Saturation
% 13.22/2.99 % (2033897)Time elapsed: 0.083 s
% 13.22/2.99 % (2033897)Peak memory usage: 91 MB
% 13.22/2.99 % (2033897)Instructions burned: 249 (million)
% 13.22/2.99 % (2033898)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4091566394:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 13.22/2.99 % (2033898)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033898)------------------------------
% 13.22/2.99 % (2033898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033898)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033898)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033898)Time elapsed: 0.002 s
% 13.22/2.99 % (2033898)Peak memory usage: 88 MB
% 13.22/2.99 % (2033898)Instructions burned: 1 (million)
% 13.22/2.99 % (2033902)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2397627604:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 13.22/2.99 % (2033902)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033902)------------------------------
% 13.22/2.99 % (2033902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033902)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033902)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033902)Time elapsed: 0.001 s
% 13.22/2.99 % (2033902)Peak memory usage: 88 MB
% 13.22/2.99 % (2033902)Instructions burned: 1 (million)
% 13.22/2.99 % (2033901)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=909233622:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 13.22/2.99 % (2033880)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033880)------------------------------
% 13.22/2.99 % (2033880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033880)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033880)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033880)Time elapsed: 0.607 s
% 13.22/2.99 % (2033880)Peak memory usage: 126 MB
% 13.22/2.99 % (2033880)Instructions burned: 895 (million)
% 13.22/2.99 % (2033896)Instruction limit reached!
% 13.22/2.99 % (2033896)------------------------------
% 13.22/2.99 % (2033896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033896)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033896)Termination reason: Instruction limit
% 13.22/2.99 % (2033896)Termination phase: Saturation
% 13.22/2.99 % (2033896)Time elapsed: 0.217 s
% 13.22/2.99 % (2033896)Peak memory usage: 93 MB
% 13.22/2.99 % (2033896)Instructions burned: 326 (million)
% 13.22/2.99 % (2033902)------------------------------
% 13.22/2.99 % (2033902)------------------------------
% 13.22/2.99 % (2033898)------------------------------
% 13.22/2.99 % (2033898)------------------------------
% 13.22/2.99 % (2033906)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=626665101:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 13.22/2.99 % (2033906)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033906)------------------------------
% 13.22/2.99 % (2033906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033906)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033906)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033906)Time elapsed: 0.001 s
% 13.22/2.99 % (2033906)Peak memory usage: 88 MB
% 13.22/2.99 % (2033907)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3836758564:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 13.22/2.99 % (2033907)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033907)------------------------------
% 13.22/2.99 % (2033907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033907)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033907)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033907)Time elapsed: 0.001 s
% 13.22/2.99 % (2033907)Peak memory usage: 88 MB
% 13.22/2.99 % (2033880)------------------------------
% 13.22/2.99 % (2033880)------------------------------
% 13.22/2.99 % (2033908)lrs+10_1_sil=8000:sp=occurrence:random_seed=2072850458:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 13.22/2.99 % (2033907)------------------------------
% 13.22/2.99 % (2033907)------------------------------
% 13.22/2.99 % (2033911)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2648275665:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 13.22/2.99 % (2033911)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033911)------------------------------
% 13.22/2.99 % (2033911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033911)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033911)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033911)Time elapsed: 0.001 s
% 13.22/2.99 % (2033911)Peak memory usage: 88 MB
% 13.22/2.99 % (2033906)------------------------------
% 13.22/2.99 % (2033906)------------------------------
% 13.22/2.99 % (2033913)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4022652396:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 13.22/2.99 % (2033915)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1876965715:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 13.22/2.99 % (2033915)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033915)------------------------------
% 13.22/2.99 % (2033915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033915)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033915)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033915)Time elapsed: 0.002 s
% 13.22/2.99 % (2033915)Peak memory usage: 89 MB
% 13.22/2.99 % (2033915)Instructions burned: 1 (million)
% 13.22/2.99 % (2033911)------------------------------
% 13.22/2.99 % (2033911)------------------------------
% 13.22/2.99 % (2033918)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=974400966:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 13.22/2.99 % (2033918)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033918)------------------------------
% 13.22/2.99 % (2033918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033918)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033918)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033918)Time elapsed: 0.001 s
% 13.22/2.99 % (2033918)Peak memory usage: 88 MB
% 13.22/2.99 % (2033908)Instruction limit reached!
% 13.22/2.99 % (2033908)------------------------------
% 13.22/2.99 % (2033908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033908)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033908)Termination reason: Instruction limit
% 13.22/2.99 % (2033908)Termination phase: Saturation
% 13.22/2.99 % (2033908)Time elapsed: 0.542 s
% 13.22/2.99 % (2033908)Peak memory usage: 96 MB
% 13.22/2.99 % (2033908)Instructions burned: 908 (million)
% 13.22/2.99 % (2033915)------------------------------
% 13.22/2.99 % (2033915)------------------------------
% 13.22/2.99 % (2033920)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=665058878:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 13.22/2.99 % (2033921)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=291736655:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 13.22/2.99 % (2033918)------------------------------
% 13.22/2.99 % (2033918)------------------------------
% 13.22/2.99 % (2033921)Instruction limit reached!
% 13.22/2.99 % (2033921)------------------------------
% 13.22/2.99 % (2033921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033921)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033921)Termination reason: Instruction limit
% 13.22/2.99 % (2033921)Termination phase: Saturation
% 13.22/2.99 % (2033921)Time elapsed: 0.083 s
% 13.22/2.99 % (2033921)Peak memory usage: 90 MB
% 13.22/2.99 % (2033921)Instructions burned: 127 (million)
% 13.22/2.99 % (2033913)First to succeed.
% 13.22/2.99 % (2033913)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2033873"
% 13.22/2.99 % (2033924)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2175876807:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 13.22/2.99 % (2033925)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3556036980:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 13.22/2.99 % (2033925)Refutation not found, incomplete strategy
% 13.22/2.99 % (2033925)------------------------------
% 13.22/2.99 % (2033925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.99 % (2033925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.99 % (2033925)CaDiCaL version: 2.1.3
% 13.22/2.99 % (2033925)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.99 % (2033925)Time elapsed: 0.001 s
% 13.22/2.99 % (2033925)Peak memory usage: 88 MB
% 13.22/2.99 % (2033913)Refutation found. Thanks to Tanya!
% 13.22/2.99 % SZS status Theorem for theBenchmark
% 13.22/2.99 % SZS output start Proof for theBenchmark
% See solution above
% 15.42/3.19 % (2033913)------------------------------
% 15.42/3.19 % (2033913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.42/3.19 % (2033913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/3.19 % (2033913)CaDiCaL version: 2.1.3
% 15.42/3.19 % (2033913)Termination reason: Refutation
% 15.42/3.19 % (2033913)Time elapsed: 0.622 s
% 15.42/3.19 % (2033913)Peak memory usage: 138 MB
% 15.42/3.19 % (2033913)Instructions burned: 1766 (million)
% 15.42/3.19 % (2033913)------------------------------
% 15.42/3.19 % (2033913)------------------------------
% 15.42/3.19 % (2033873)Success in time 2.098 s
% 15.42/3.19 % Vampire exiting
%------------------------------------------------------------------------------