%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : KLE145+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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:59 AM UTC 2026
% Result : Theorem 249.60s 39.24s
% Output : Refutation 249.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 17
% Syntax : Number of formulae : 131 ( 86 unt; 2 def)
% Number of atoms : 178 ( 86 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 90 ( 43 ~; 39 |; 3 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 237 ( 0 sgn 236 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',additive_associativity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',multiplicative_left_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',distributivity1) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',distributivity2) ).
fof(f11,axiom,
! [X0] : addition(one,multiplication(X0,star(X0))) = star(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',star_unfold1) ).
fof(f12,axiom,
! [X0] : addition(one,multiplication(star(X0),X0)) = star(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',star_unfold2) ).
fof(f14,axiom,
! [X0,X1,X2] :
( leq(addition(multiplication(X2,X0),X1),X2)
=> leq(multiplication(X1,star(X0)),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',star_induction2) ).
fof(f15,axiom,
! [X0] : strong_iteration(X0) = addition(multiplication(X0,strong_iteration(X0)),one),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',infty_unfold1) ).
fof(f16,axiom,
! [X0,X1,X2] :
( leq(X2,addition(multiplication(X0,X2),X1))
=> leq(X2,multiplication(strong_iteration(X0),X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',infty_coinduction) ).
fof(f18,axiom,
! [X0,X1] :
( leq(X0,X1)
<=> addition(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE004+0.ax',order) ).
fof(f19,conjecture,
! [X0] :
( leq(star(strong_iteration(X0)),strong_iteration(X0))
& leq(strong_iteration(X0),star(strong_iteration(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f20,negated_conjecture,
~ ! [X0] :
( leq(star(strong_iteration(X0)),strong_iteration(X0))
& leq(strong_iteration(X0),star(strong_iteration(X0))) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f22,plain,
! [X0,X1,X2] :
( leq(multiplication(X1,star(X0)),X2)
| ~ leq(addition(multiplication(X2,X0),X1),X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f23,plain,
! [X0,X1,X2] :
( leq(X2,multiplication(strong_iteration(X0),X1))
| ~ leq(X2,addition(multiplication(X0,X2),X1)) ),
inference(ennf_transformation,[],[f16]) ).
fof(f24,plain,
? [X0] :
( ~ leq(star(strong_iteration(X0)),strong_iteration(X0))
| ~ leq(strong_iteration(X0),star(strong_iteration(X0))) ),
inference(ennf_transformation,[],[f20]) ).
fof(f25,plain,
! [X0,X1] :
( ( leq(X0,X1)
| addition(X0,X1) != X1 )
& ( addition(X0,X1) = X1
| ~ leq(X0,X1) ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f26,plain,
( ~ leq(star(strong_iteration(sK0)),strong_iteration(sK0))
| ~ leq(strong_iteration(sK0),star(strong_iteration(sK0))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f24]) ).
fof(f27,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f28,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f30,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f31,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f32,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f33,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f34,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f37,plain,
! [X0] : star(X0) = addition(one,multiplication(X0,star(X0))),
inference(cnf_transformation,[],[f11]) ).
fof(f38,plain,
! [X0] : star(X0) = addition(one,multiplication(star(X0),X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f40,plain,
! [X2,X0,X1] :
( leq(multiplication(X1,star(X0)),X2)
| ~ leq(addition(multiplication(X2,X0),X1),X2) ),
inference(cnf_transformation,[],[f22]) ).
fof(f41,plain,
! [X0] : strong_iteration(X0) = addition(multiplication(X0,strong_iteration(X0)),one),
inference(cnf_transformation,[],[f15]) ).
fof(f42,plain,
! [X2,X0,X1] :
( leq(X2,multiplication(strong_iteration(X0),X1))
| ~ leq(X2,addition(multiplication(X0,X2),X1)) ),
inference(cnf_transformation,[],[f23]) ).
fof(f44,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| addition(X0,X1) = X1 ),
inference(cnf_transformation,[],[f25]) ).
fof(f45,plain,
! [X0,X1] :
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f46,plain,
( ~ leq(star(strong_iteration(sK0)),strong_iteration(sK0))
| ~ leq(strong_iteration(sK0),star(strong_iteration(sK0))) ),
inference(cnf_transformation,[],[f26]) ).
fof(f48,definition,
( spl1_1
<=> leq(strong_iteration(sK0),star(strong_iteration(sK0))) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f50,plain,
( ~ leq(strong_iteration(sK0),star(strong_iteration(sK0)))
| spl1_1 ),
inference(avatar_component_clause,[],[f48]) ).
fof(f52,definition,
( spl1_2
<=> leq(star(strong_iteration(sK0)),strong_iteration(sK0)) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
fof(f54,plain,
( ~ leq(star(strong_iteration(sK0)),strong_iteration(sK0))
| spl1_2 ),
inference(avatar_component_clause,[],[f52]) ).
fof(f55,plain,
( ~ spl1_1
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f46,f52,f48]) ).
fof(f114,plain,
! [X0] : strong_iteration(X0) = addition(one,multiplication(X0,strong_iteration(X0))),
inference(superposition,[],[f27,f41]) ).
fof(f157,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f28,f30]) ).
fof(f159,plain,
! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2)),
inference(superposition,[],[f28,f27]) ).
fof(f162,plain,
! [X0,X1] : addition(multiplication(X0,strong_iteration(X0)),addition(one,X1)) = addition(strong_iteration(X0),X1),
inference(superposition,[],[f28,f41]) ).
fof(f176,plain,
! [X2,X0,X1] :
( leq(addition(X0,X1),X2)
| addition(X0,addition(X1,X2)) != X2 ),
inference(superposition,[],[f45,f28]) ).
fof(f178,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f27,f28]) ).
fof(f179,plain,
! [X0,X1] : addition(strong_iteration(X0),X1) = addition(one,addition(X1,multiplication(X0,strong_iteration(X0)))),
inference(forward_demodulation,[],[f162,f178]) ).
fof(f191,plain,
! [X0] : strong_iteration(X0) = addition(one,strong_iteration(X0)),
inference(superposition,[],[f157,f114]) ).
fof(f192,plain,
! [X0] : star(X0) = addition(one,star(X0)),
inference(superposition,[],[f157,f38]) ).
fof(f199,plain,
! [X0,X1] :
( addition(X0,X1) != addition(X0,X1)
| leq(X0,addition(X0,X1)) ),
inference(superposition,[],[f45,f157]) ).
fof(f201,plain,
! [X0,X1] : leq(X0,addition(X0,X1)),
inference(trivial_inequality_removal,[],[f199]) ).
fof(f213,plain,
! [X0,X1] : leq(X1,addition(X0,X1)),
inference(superposition,[],[f201,f27]) ).
fof(f233,plain,
! [X2,X0,X1] : leq(X2,addition(X0,addition(X1,X2))),
inference(superposition,[],[f213,f28]) ).
fof(f238,plain,
! [X0] : leq(multiplication(star(X0),X0),star(X0)),
inference(superposition,[],[f213,f38]) ).
fof(f284,plain,
! [X2,X0,X1] : leq(X0,addition(X2,addition(X0,X1))),
inference(superposition,[],[f233,f27]) ).
fof(f289,plain,
! [X0,X1] : leq(one,addition(X1,strong_iteration(X0))),
inference(superposition,[],[f233,f41]) ).
fof(f308,plain,
! [X0,X1] : leq(one,addition(strong_iteration(X0),X1)),
inference(superposition,[],[f289,f27]) ).
fof(f309,plain,
! [X2,X0,X1] : leq(one,addition(X0,addition(X1,strong_iteration(X2)))),
inference(superposition,[],[f289,f28]) ).
fof(f326,plain,
! [X0] : star(X0) = addition(multiplication(star(X0),X0),star(X0)),
inference(resolution,[],[f238,f44]) ).
fof(f330,plain,
! [X0] : star(X0) = addition(star(X0),multiplication(star(X0),X0)),
inference(forward_demodulation,[],[f326,f27]) ).
fof(f358,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f34,f32]) ).
fof(f371,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1)),
inference(superposition,[],[f27,f34]) ).
fof(f459,plain,
! [X2,X0,X1] : leq(one,addition(X2,addition(strong_iteration(X0),X1))),
inference(superposition,[],[f309,f27]) ).
fof(f474,plain,
! [X2,X3,X0,X1] : multiplication(addition(multiplication(X0,X1),X3),X2) = addition(multiplication(X0,multiplication(X1,X2)),multiplication(X3,X2)),
inference(superposition,[],[f35,f31]) ).
fof(f475,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f35,f33]) ).
fof(f479,plain,
! [X0,X1] : multiplication(addition(X1,one),X0) = addition(multiplication(X1,X0),X0),
inference(superposition,[],[f35,f33]) ).
fof(f487,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2)),
inference(superposition,[],[f27,f35]) ).
fof(f488,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,X2),addition(multiplication(X1,X2),X3)) = addition(multiplication(addition(X0,X1),X2),X3),
inference(superposition,[],[f28,f35]) ).
fof(f499,plain,
! [X0,X1] : addition(X0,multiplication(X1,X0)) = multiplication(addition(X1,one),X0),
inference(forward_demodulation,[],[f479,f27]) ).
fof(f1009,plain,
! [X0,X1] :
( leq(star(X0),X1)
| ~ leq(addition(multiplication(X1,X0),one),X1) ),
inference(superposition,[],[f40,f33]) ).
fof(f1010,plain,
! [X0,X1] :
( leq(star(X0),X1)
| ~ leq(addition(one,multiplication(X1,X0)),X1) ),
inference(forward_demodulation,[],[f1009,f27]) ).
fof(f1120,plain,
! [X0,X1] :
( leq(X1,strong_iteration(X0))
| ~ leq(X1,addition(multiplication(X0,X1),one)) ),
inference(superposition,[],[f42,f32]) ).
fof(f1121,plain,
! [X0,X1] :
( leq(X1,strong_iteration(X0))
| ~ leq(X1,addition(one,multiplication(X0,X1))) ),
inference(forward_demodulation,[],[f1120,f27]) ).
fof(f1442,plain,
! [X2,X3,X0,X1] : addition(addition(X0,addition(X1,X2)),X3) = addition(X2,addition(addition(X1,X0),X3)),
inference(superposition,[],[f159,f159]) ).
fof(f1462,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X1,addition(X0,X2)),
inference(superposition,[],[f28,f159]) ).
fof(f1549,plain,
! [X2,X3,X0,X1] : addition(addition(X0,addition(X1,X2)),X3) = addition(X2,addition(X1,addition(X0,X3))),
inference(forward_demodulation,[],[f1442,f28]) ).
fof(f1559,plain,
! [X2,X3,X0,X1] : addition(X0,addition(addition(X1,X2),X3)) = addition(X2,addition(X1,addition(X0,X3))),
inference(forward_demodulation,[],[f1549,f28]) ).
fof(f1565,plain,
! [X2,X3,X0,X1] : addition(X0,addition(X1,addition(X2,X3))) = addition(X2,addition(X1,addition(X0,X3))),
inference(forward_demodulation,[],[f1559,f28]) ).
fof(f3000,plain,
! [X2,X0,X1] : leq(X0,addition(X2,multiplication(X0,addition(one,X1)))),
inference(superposition,[],[f284,f358]) ).
fof(f3520,plain,
! [X2,X0,X1] : multiplication(addition(one,multiplication(X0,X1)),X2) = addition(X2,multiplication(X0,multiplication(X1,X2))),
inference(superposition,[],[f475,f31]) ).
fof(f3535,plain,
! [X2,X0,X1] : addition(multiplication(addition(one,X0),X1),X2) = addition(multiplication(X0,X1),addition(X1,X2)),
inference(superposition,[],[f159,f475]) ).
fof(f3588,plain,
! [X0,X1] : leq(one,multiplication(addition(one,X0),strong_iteration(X1))),
inference(superposition,[],[f308,f475]) ).
fof(f3628,plain,
! [X2,X0,X1] : addition(multiplication(addition(one,X0),X1),X2) = addition(X1,addition(X2,multiplication(X0,X1))),
inference(forward_demodulation,[],[f3535,f178]) ).
fof(f3881,plain,
! [X2,X0,X1] : leq(one,addition(X2,multiplication(addition(X0,one),strong_iteration(X1)))),
inference(superposition,[],[f459,f499]) ).
fof(f4031,plain,
! [X0,X1] : multiplication(addition(one,X0),strong_iteration(X1)) = addition(one,multiplication(addition(one,X0),strong_iteration(X1))),
inference(resolution,[],[f3588,f44]) ).
fof(f4801,plain,
! [X2,X0,X1] :
( leq(multiplication(addition(one,X0),X1),X2)
| addition(X1,addition(multiplication(X0,X1),X2)) != X2 ),
inference(superposition,[],[f176,f475]) ).
fof(f5361,plain,
! [X2,X0,X1] : leq(X1,addition(X2,multiplication(X1,star(X0)))),
inference(superposition,[],[f3000,f192]) ).
fof(f5445,plain,
! [X0] : leq(X0,star(X0)),
inference(superposition,[],[f5361,f37]) ).
fof(f5448,plain,
( $false
| spl1_1 ),
inference(resolution,[],[f5445,f50]) ).
fof(f5449,plain,
! [X0] : star(X0) = addition(X0,star(X0)),
inference(resolution,[],[f5445,f44]) ).
fof(f5451,plain,
spl1_1,
inference(avatar_contradiction_clause,[],[f5448]) ).
fof(f5452,plain,
( ~ leq(star(strong_iteration(sK0)),addition(one,multiplication(sK0,star(strong_iteration(sK0)))))
| spl1_2 ),
inference(resolution,[],[f54,f1121]) ).
fof(f5458,plain,
( ~ leq(addition(one,multiplication(addition(one,multiplication(sK0,star(strong_iteration(sK0)))),strong_iteration(sK0))),addition(one,multiplication(sK0,star(strong_iteration(sK0)))))
| spl1_2 ),
inference(resolution,[],[f5452,f1010]) ).
fof(f5461,plain,
( ~ leq(multiplication(addition(one,multiplication(sK0,star(strong_iteration(sK0)))),strong_iteration(sK0)),addition(one,multiplication(sK0,star(strong_iteration(sK0)))))
| spl1_2 ),
inference(forward_demodulation,[],[f5458,f4031]) ).
fof(f6573,plain,
! [X0,X1] : addition(strong_iteration(X0),multiplication(X0,X1)) = addition(one,multiplication(X0,addition(strong_iteration(X0),X1))),
inference(superposition,[],[f179,f371]) ).
fof(f6865,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = multiplication(addition(X1,X0),X2),
inference(superposition,[],[f35,f487]) ).
fof(f10758,plain,
! [X2,X3,X0,X1] : addition(multiplication(addition(X3,X1),X2),multiplication(X0,X2)) = addition(multiplication(X3,X2),multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f488,f487]) ).
fof(f10947,plain,
! [X2,X3,X0,X1] : addition(multiplication(addition(X3,X1),X2),multiplication(X0,X2)) = multiplication(addition(X3,addition(X0,X1)),X2),
inference(forward_demodulation,[],[f10758,f35]) ).
fof(f10998,plain,
! [X2,X3,X0,X1] : multiplication(addition(X3,addition(X0,X1)),X2) = multiplication(addition(addition(X3,X1),X0),X2),
inference(forward_demodulation,[],[f10947,f35]) ).
fof(f11028,plain,
! [X2,X3,X0,X1] : multiplication(addition(X3,addition(X0,X1)),X2) = multiplication(addition(X3,addition(X1,X0)),X2),
inference(forward_demodulation,[],[f10998,f28]) ).
fof(f13685,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X0,addition(X2,X1)),
inference(superposition,[],[f178,f1462]) ).
fof(f17792,plain,
! [X2,X3,X0,X1] : multiplication(addition(X0,addition(X1,X2)),X3) = multiplication(addition(X2,addition(X0,X1)),X3),
inference(superposition,[],[f6865,f28]) ).
fof(f48745,plain,
! [X0] : star(X0) = multiplication(star(X0),addition(one,X0)),
inference(superposition,[],[f358,f330]) ).
fof(f49181,plain,
! [X0] : star(strong_iteration(X0)) = multiplication(star(strong_iteration(X0)),strong_iteration(X0)),
inference(superposition,[],[f48745,f191]) ).
fof(f72675,plain,
! [X2,X3,X0,X1,X4] : addition(X0,addition(multiplication(X1,X2),addition(multiplication(X3,X2),X4))) = addition(multiplication(addition(X3,X1),X2),addition(X0,X4)),
inference(superposition,[],[f488,f1565]) ).
fof(f73019,plain,
! [X2,X3,X0,X1,X4] : addition(X0,addition(multiplication(addition(X1,X3),X2),X4)) = addition(multiplication(addition(X3,X1),X2),addition(X0,X4)),
inference(forward_demodulation,[],[f72675,f488]) ).
fof(f88000,plain,
! [X2,X0,X1] : multiplication(addition(multiplication(X1,star(strong_iteration(X0))),X2),strong_iteration(X0)) = addition(multiplication(X1,star(strong_iteration(X0))),multiplication(X2,strong_iteration(X0))),
inference(superposition,[],[f474,f49181]) ).
fof(f102058,plain,
! [X2,X0,X1] : addition(X0,multiplication(addition(X1,one),strong_iteration(X2))) = addition(one,addition(X0,multiplication(addition(X1,one),strong_iteration(X2)))),
inference(resolution,[],[f3881,f44]) ).
fof(f122193,plain,
! [X0,X1] : addition(strong_iteration(X0),multiplication(X1,star(strong_iteration(X0)))) = multiplication(addition(one,multiplication(X1,star(strong_iteration(X0)))),strong_iteration(X0)),
inference(superposition,[],[f3520,f49181]) ).
fof(f171269,plain,
! [X0] : addition(one,multiplication(X0,star(strong_iteration(X0)))) = addition(strong_iteration(X0),multiplication(X0,star(strong_iteration(X0)))),
inference(superposition,[],[f6573,f5449]) ).
fof(f211381,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != addition(strong_iteration(sK0),addition(multiplication(multiplication(sK0,star(strong_iteration(sK0))),strong_iteration(sK0)),addition(one,multiplication(sK0,star(strong_iteration(sK0))))))
| spl1_2 ),
inference(resolution,[],[f4801,f5461]) ).
fof(f211600,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != addition(strong_iteration(sK0),addition(addition(one,multiplication(sK0,star(strong_iteration(sK0)))),multiplication(multiplication(sK0,star(strong_iteration(sK0))),strong_iteration(sK0))))
| spl1_2 ),
inference(forward_demodulation,[],[f211381,f13685]) ).
fof(f211666,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != addition(multiplication(addition(one,multiplication(sK0,star(strong_iteration(sK0)))),strong_iteration(sK0)),addition(one,multiplication(sK0,star(strong_iteration(sK0)))))
| spl1_2 ),
inference(forward_demodulation,[],[f211600,f3628]) ).
fof(f211705,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != addition(one,addition(multiplication(addition(multiplication(sK0,star(strong_iteration(sK0))),one),strong_iteration(sK0)),multiplication(sK0,star(strong_iteration(sK0)))))
| spl1_2 ),
inference(forward_demodulation,[],[f211666,f73019]) ).
fof(f211723,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != addition(one,addition(multiplication(sK0,star(strong_iteration(sK0))),multiplication(addition(multiplication(sK0,star(strong_iteration(sK0))),one),strong_iteration(sK0))))
| spl1_2 ),
inference(forward_demodulation,[],[f211705,f13685]) ).
fof(f211733,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != addition(multiplication(sK0,star(strong_iteration(sK0))),multiplication(addition(multiplication(sK0,star(strong_iteration(sK0))),one),strong_iteration(sK0)))
| spl1_2 ),
inference(forward_demodulation,[],[f211723,f102058]) ).
fof(f211738,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != multiplication(addition(multiplication(sK0,star(strong_iteration(sK0))),addition(multiplication(sK0,star(strong_iteration(sK0))),one)),strong_iteration(sK0))
| spl1_2 ),
inference(forward_demodulation,[],[f211733,f88000]) ).
fof(f211741,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != multiplication(addition(multiplication(sK0,star(strong_iteration(sK0))),addition(one,multiplication(sK0,star(strong_iteration(sK0))))),strong_iteration(sK0))
| spl1_2 ),
inference(forward_demodulation,[],[f211738,f11028]) ).
fof(f211743,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != multiplication(addition(one,addition(multiplication(sK0,star(strong_iteration(sK0))),multiplication(sK0,star(strong_iteration(sK0))))),strong_iteration(sK0))
| spl1_2 ),
inference(forward_demodulation,[],[f211741,f17792]) ).
fof(f211744,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != multiplication(addition(one,multiplication(addition(sK0,sK0),star(strong_iteration(sK0)))),strong_iteration(sK0))
| spl1_2 ),
inference(forward_demodulation,[],[f211743,f35]) ).
fof(f211745,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != addition(strong_iteration(sK0),multiplication(addition(sK0,sK0),star(strong_iteration(sK0))))
| spl1_2 ),
inference(forward_demodulation,[],[f211744,f122193]) ).
fof(f211746,plain,
( addition(one,multiplication(sK0,star(strong_iteration(sK0)))) != addition(strong_iteration(sK0),multiplication(sK0,star(strong_iteration(sK0))))
| spl1_2 ),
inference(forward_demodulation,[],[f211745,f30]) ).
fof(f211747,plain,
( $false
| spl1_2 ),
inference(forward_subsumption_resolution,[],[f211746,f171269]) ).
fof(f211748,plain,
spl1_2,
inference(avatar_contradiction_clause,[],[f211747]) ).
cnf(s1,plain,
( ~ spl1_1
| ~ spl1_2 ),
inference(sat_conversion,[],[f55]) ).
cnf(s4,plain,
spl1_1,
inference(sat_conversion,[],[f5451]) ).
cnf(s19,plain,
spl1_2,
inference(sat_conversion,[],[f211748]) ).
cnf(s27,plain,
$false,
inference(rat,[],[s1,s19,s4]) ).
fof(f211749,plain,
$false,
inference(avatar_sat_refutation,[],[s27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE145+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n005.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 13:12:17 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.40 Running first-order model finding
% 0.12/0.40 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
% 14.83/2.54 % (3983671)Will run a generic schedule for satisfiability detection.
% 14.83/2.54 % (3983680)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2179751590:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.83/2.54 % (3983677)% WARNING: option uhcvi not known.
% 14.83/2.54 % (3983676)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=511959655_2999 on theBenchmark for (2999ds/0Mi)
% 14.83/2.54 % (3983682)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=895441109:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.83/2.54 % (3983678)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4214056855:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.83/2.54 % (3983679)dis+10_1_sil=32000:sp=arity:random_seed=1622029836:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.83/2.54 % (3983681)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3661925765:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.83/2.54 % (3983677)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3113708672:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.83/2.54 % TRYING [1]
% 14.83/2.54 % TRYING [2]
% 14.83/2.54 % TRYING [3]
% 14.83/2.54 % TRYING [4]
% 14.83/2.54 % TRYING [5]
% 14.83/2.54 % (3983680)Instruction limit reached!
% 14.83/2.54 % (3983680)------------------------------
% 14.83/2.54 % (3983680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.83/2.54 % (3983680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/2.54 % (3983680)CaDiCaL version: 2.1.3
% 14.83/2.54 % (3983680)Termination reason: Instruction limit
% 14.83/2.54 % (3983680)Termination phase: Saturation
% 14.83/2.54 % (3983680)Time elapsed: 0.041 s
% 14.83/2.54 % (3983680)Peak memory usage: 13 MB
% 14.83/2.54 % (3983680)Instructions burned: 119 (million)
% 14.83/2.54 % (3983690)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4235847525:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.83/2.54 % TRYING [1]
% 14.83/2.54 % TRYING [2]
% 14.83/2.54 % TRYING [3]
% 14.83/2.54 % TRYING [4]
% 14.83/2.54 % (3983679)Instruction limit reached!
% 14.83/2.54 % (3983679)------------------------------
% 14.83/2.54 % (3983679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.83/2.54 % (3983679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/2.54 % (3983679)CaDiCaL version: 2.1.3
% 14.83/2.54 % (3983679)Termination reason: Instruction limit
% 14.83/2.54 % (3983679)Termination phase: Saturation
% 14.83/2.54 % (3983679)Time elapsed: 0.064 s
% 14.83/2.54 % (3983679)Peak memory usage: 12 MB
% 14.83/2.54 % (3983679)Instructions burned: 104 (million)
% 14.83/2.54 % (3983681)Instruction limit reached!
% 14.83/2.54 % (3983681)------------------------------
% 14.83/2.54 % (3983681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.83/2.54 % (3983681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/2.54 % (3983681)CaDiCaL version: 2.1.3
% 14.83/2.54 % (3983681)Termination reason: Instruction limit
% 14.83/2.54 % (3983681)Termination phase: Saturation
% 14.83/2.54 % (3983681)Time elapsed: 0.082 s
% 14.83/2.54 % (3983681)Peak memory usage: 13 MB
% 14.83/2.54 % (3983681)Instructions burned: 132 (million)
% 14.83/2.54 % (3983692)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2863780434:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.83/2.54 % TRYING [5]
% 14.83/2.54 % TRYING [6]
% 14.83/2.54 % (3983694)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=4129639812:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.83/2.54 % (3983682)Instruction limit reached!
% 14.83/2.54 % (3983682)------------------------------
% 14.83/2.54 % (3983682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.83/2.54 % (3983682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/2.54 % (3983682)CaDiCaL version: 2.1.3
% 14.83/2.54 % (3983682)Termination reason: Instruction limit
% 14.83/2.54 % (3983682)Termination phase: Saturation
% 14.83/2.54 % (3983682)Time elapsed: 0.106 s
% 14.83/2.54 % (3983682)Peak memory usage: 13 MB
% 14.83/2.54 % (3983682)Instructions burned: 160 (million)
% 14.83/2.54 % (3983696)ott-21_1_sil=16000:fs=off:random_seed=2165124345:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.83/2.54 % TRYING [6]
% 14.83/2.54 % (3983692)Instruction limit reached!
% 14.83/2.54 % (3983692)------------------------------
% 14.83/2.54 % (3983692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.88/6.10 % (3983692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.10 % (3983692)CaDiCaL version: 2.1.3
% 39.88/6.10 % (3983692)Termination reason: Instruction limit
% 39.88/6.10 % (3983692)Termination phase: Saturation
% 39.88/6.10 % (3983692)Time elapsed: 0.089 s
% 39.88/6.10 % (3983692)Peak memory usage: 13 MB
% 39.88/6.10 % (3983692)Instructions burned: 132 (million)
% 39.88/6.10 % (3983698)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=298797303:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 39.88/6.10 % (3983696)Instruction limit reached!
% 39.88/6.10 % (3983696)------------------------------
% 39.88/6.10 % (3983696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.88/6.10 % (3983696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.10 % (3983696)CaDiCaL version: 2.1.3
% 39.88/6.10 % (3983696)Termination reason: Instruction limit
% 39.88/6.10 % (3983696)Termination phase: Saturation
% 39.88/6.10 % (3983696)Time elapsed: 0.077 s
% 39.88/6.10 % (3983696)Peak memory usage: 12 MB
% 39.88/6.10 % (3983696)Instructions burned: 181 (million)
% 39.88/6.10 % (3983700)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2161464302:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 39.88/6.10 % TRYING [1]
% 39.88/6.10 % TRYING [2]
% 39.88/6.10 % TRYING [3]
% 39.88/6.10 % TRYING [4]
% 39.88/6.10 % (3983690)Instruction limit reached!
% 39.88/6.10 % (3983690)------------------------------
% 39.88/6.10 % (3983690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.88/6.10 % (3983690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.10 % (3983690)CaDiCaL version: 2.1.3
% 39.88/6.10 % (3983690)Termination reason: Instruction limit
% 39.88/6.10 % (3983690)Termination phase: Finite model building SAT solving
% 39.88/6.10 % (3983690)Time elapsed: 0.196 s
% 39.88/6.10 % (3983690)Peak memory usage: 32 MB
% 39.88/6.10 % (3983690)Instructions burned: 716 (million)
% 39.88/6.10 % TRYING [7]
% 39.88/6.10 % (3983702)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2547078123:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 39.88/6.10 % TRYING [5]
% 39.88/6.10 % TRYING [6]
% 39.88/6.10 % (3983694)Instruction limit reached!
% 39.88/6.10 % (3983694)------------------------------
% 39.88/6.10 % (3983694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.88/6.10 % (3983694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.10 % (3983694)CaDiCaL version: 2.1.3
% 39.88/6.10 % (3983694)Termination reason: Instruction limit
% 39.88/6.10 % (3983694)Termination phase: Saturation
% 39.88/6.10 % (3983694)Time elapsed: 0.366 s
% 39.88/6.10 % (3983694)Peak memory usage: 17 MB
% 39.88/6.10 % (3983694)Instructions burned: 685 (million)
% 39.88/6.10 % (3983704)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3160260393:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 39.88/6.10 % (3983698)Instruction limit reached!
% 39.88/6.10 % (3983698)------------------------------
% 39.88/6.10 % (3983698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.88/6.10 % (3983698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.10 % (3983698)CaDiCaL version: 2.1.3
% 39.88/6.10 % (3983698)Termination reason: Instruction limit
% 39.88/6.10 % (3983698)Termination phase: Saturation
% 39.88/6.10 % (3983698)Time elapsed: 0.302 s
% 39.88/6.10 % (3983698)Peak memory usage: 14 MB
% 39.88/6.10 % (3983698)Instructions burned: 478 (million)
% 39.88/6.10 % (3983706)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=554920253: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)
% 39.88/6.10 % (3983700)Instruction limit reached!
% 39.88/6.10 % (3983700)------------------------------
% 39.88/6.10 % (3983700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.88/6.10 % (3983700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.10 % (3983700)CaDiCaL version: 2.1.3
% 39.88/6.10 % (3983700)Termination reason: Instruction limit
% 39.88/6.10 % (3983700)Termination phase: Finite model building SAT solving
% 39.88/6.10 % (3983700)Time elapsed: 0.336 s
% 39.88/6.10 % (3983700)Peak memory usage: 25 MB
% 39.88/6.10 % (3983700)Instructions burned: 865 (million)
% 39.88/6.10 % TRYING [8]
% 39.88/6.10 % (3983708)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1906521885:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 87.16/12.79 % TRYING [14]
% 87.16/12.79 % (3983702)Instruction limit reached!
% 87.16/12.79 % (3983702)------------------------------
% 87.16/12.79 % (3983702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.79 % (3983702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.79 % (3983702)CaDiCaL version: 2.1.3
% 87.16/12.79 % (3983702)Termination reason: Instruction limit
% 87.16/12.79 % (3983702)Termination phase: Saturation
% 87.16/12.79 % (3983702)Time elapsed: 0.396 s
% 87.16/12.79 % (3983702)Peak memory usage: 23 MB
% 87.16/12.79 % (3983702)Instructions burned: 1181 (million)
% 87.16/12.79 % (3983710)fmb+10_1_sil=64000:random_seed=1089724144:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 87.16/12.79 % TRYING [1]
% 87.16/12.79 % TRYING [2]
% 87.16/12.79 % TRYING [3]
% 87.16/12.79 % TRYING [4]
% 87.16/12.79 % TRYING [5]
% 87.16/12.79 % TRYING [6]
% 87.16/12.79 % (3983704)Instruction limit reached!
% 87.16/12.79 % (3983704)------------------------------
% 87.16/12.79 % (3983704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.79 % (3983704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.79 % (3983704)CaDiCaL version: 2.1.3
% 87.16/12.79 % (3983704)Termination reason: Instruction limit
% 87.16/12.79 % (3983704)Termination phase: Finite model building constraint generation
% 87.16/12.79 % (3983704)Time elapsed: 0.346 s
% 87.16/12.79 % (3983704)Peak memory usage: 82 MB
% 87.16/12.79 % (3983704)Instructions burned: 892 (million)
% 87.16/12.79 % (3983712)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1974825902:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 87.16/12.79 % TRYING [20]
% 87.16/12.79 % TRYING [7]
% 87.16/12.79 % (3983706)Instruction limit reached!
% 87.16/12.79 % (3983706)------------------------------
% 87.16/12.79 % (3983706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.79 % (3983706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.79 % (3983706)CaDiCaL version: 2.1.3
% 87.16/12.79 % (3983706)Termination reason: Instruction limit
% 87.16/12.79 % (3983706)Termination phase: Saturation
% 87.16/12.79 % (3983706)Time elapsed: 0.460 s
% 87.16/12.79 % (3983706)Peak memory usage: 19 MB
% 87.16/12.79 % (3983706)Instructions burned: 692 (million)
% 87.16/12.79 % (3983714)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1704906920:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 87.16/12.79 % TRYING [8]
% 87.16/12.79 % (3983708)Instruction limit reached!
% 87.16/12.79 % (3983708)------------------------------
% 87.16/12.79 % (3983708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.79 % (3983708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.79 % (3983708)CaDiCaL version: 2.1.3
% 87.16/12.79 % (3983708)Termination reason: Instruction limit
% 87.16/12.79 % (3983708)Termination phase: Saturation
% 87.16/12.79 % (3983708)Time elapsed: 0.511 s
% 87.16/12.79 % (3983708)Peak memory usage: 19 MB
% 87.16/12.79 % (3983708)Instructions burned: 879 (million)
% 87.16/12.79 % (3983716)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1559859774:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 87.16/12.79 % TRYING [9]
% 87.16/12.79 % TRYING [8]
% 87.16/12.79 % (3983714)Instruction limit reached!
% 87.16/12.79 % (3983714)------------------------------
% 87.16/12.79 % (3983714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.79 % (3983714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.79 % (3983714)CaDiCaL version: 2.1.3
% 87.16/12.79 % (3983714)Termination reason: Instruction limit
% 87.16/12.79 % (3983714)Termination phase: Finite model building constraint generation
% 87.16/12.79 % (3983714)Time elapsed: 0.352 s
% 87.16/12.79 % (3983714)Peak memory usage: 67 MB
% 87.16/12.79 % (3983714)Instructions burned: 921 (million)
% 87.16/12.79 % (3983718)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1504534796:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 87.16/12.79 % (3983718)Instruction limit reached!
% 87.16/12.79 % (3983718)------------------------------
% 87.16/12.79 % (3983718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.16/12.79 % (3983718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.16/12.79 % (3983718)CaDiCaL version: 2.1.3
% 87.16/12.79 % (3983718)Termination reason: Instruction limit
% 87.16/12.79 % (3983718)Termination phase: Saturation
% 87.16/12.79 % (3983718)Time elapsed: 0.700 s
% 87.16/12.79 % (3983718)Peak memory usage: 26 MB
% 87.16/12.79 % (3983718)Instructions burned: 1472 (million)
% 87.16/12.79 % (3983720)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2366400492:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 247.49/35.35 % TRYING [77]
% 247.49/35.35 % TRYING [9]
% 247.49/35.35 % TRYING [10]
% 247.49/35.35 % (3983716)Instruction limit reached!
% 247.49/35.35 % (3983716)------------------------------
% 247.49/35.35 % (3983716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 247.49/35.35 % (3983716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.49/35.35 % (3983716)CaDiCaL version: 2.1.3
% 247.49/35.35 % (3983716)Termination reason: Instruction limit
% 247.49/35.35 % (3983716)Termination phase: Saturation
% 247.49/35.35 % (3983716)Time elapsed: 2.745 s
% 247.49/35.35 % (3983716)Peak memory usage: 48 MB
% 247.49/35.35 % (3983716)Instructions burned: 5133 (million)
% 247.49/35.35 % (3983722)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=374782273:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 247.49/35.35 % TRYING [16]
% 247.49/35.35 % TRYING [10]
% 247.49/35.35 % (3983720)Instruction limit reached!
% 247.49/35.35 % (3983720)------------------------------
% 247.49/35.35 % (3983720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 247.49/35.35 % (3983720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.49/35.35 % (3983720)CaDiCaL version: 2.1.3
% 247.49/35.35 % (3983720)Termination reason: Instruction limit
% 247.49/35.35 % (3983720)Termination phase: Finite model building constraint generation
% 247.49/35.35 % (3983720)Time elapsed: 2.204 s
% 247.49/35.35 % (3983720)Peak memory usage: 413 MB
% 247.49/35.35 % (3983720)Instructions burned: 6324 (million)
% 247.49/35.35 % (3983712)Instruction limit reached!
% 247.49/35.35 % (3983712)------------------------------
% 247.49/35.35 % (3983712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 247.49/35.35 % (3983712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.49/35.35 % (3983712)CaDiCaL version: 2.1.3
% 247.49/35.35 % (3983712)Termination reason: Instruction limit
% 247.49/35.35 % (3983712)Termination phase: Finite model building constraint generation
% 247.49/35.35 % (3983712)Time elapsed: 3.454 s
% 247.49/35.35 % (3983712)Peak memory usage: 670 MB
% 247.49/35.35 % (3983712)Instructions burned: 9516 (million)
% 247.49/35.35 % (3983724)ott-2_1_sil=16000:newcnf=on:random_seed=3968408999:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2956 on theBenchmark for (2956ds/869Mi)
% 247.49/35.35 % (3983726)ott+10_1_sil=32000:tgt=ground:random_seed=2592743622:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 247.49/35.35 % (3983722)Instruction limit reached!
% 247.49/35.35 % (3983722)------------------------------
% 247.49/35.35 % (3983722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 247.49/35.35 % (3983722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.49/35.35 % (3983722)CaDiCaL version: 2.1.3
% 247.49/35.35 % (3983722)Termination reason: Instruction limit
% 247.49/35.35 % (3983722)Termination phase: Finite model building constraint generation
% 247.49/35.35 % (3983722)Time elapsed: 0.733 s
% 247.49/35.35 % (3983722)Peak memory usage: 136 MB
% 247.49/35.35 % (3983722)Instructions burned: 2177 (million)
% 247.49/35.35 % (3983728)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=834140529:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 247.49/35.35 % TRYING [1]
% 247.49/35.35 % TRYING [2]
% 247.49/35.35 % TRYING [3]
% 247.49/35.35 % TRYING [4]
% 247.49/35.35 % TRYING [5]
% 247.49/35.35 % TRYING [6]
% 247.49/35.35 % (3983724)Instruction limit reached!
% 247.49/35.35 % (3983724)------------------------------
% 247.49/35.35 % (3983724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 247.49/35.35 % (3983724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.49/35.35 % (3983724)CaDiCaL version: 2.1.3
% 247.49/35.35 % (3983724)Termination reason: Instruction limit
% 247.49/35.35 % (3983724)Termination phase: Saturation
% 247.49/35.35 % (3983724)Time elapsed: 0.535 s
% 247.49/35.35 % (3983724)Peak memory usage: 20 MB
% 247.49/35.35 % (3983724)Instructions burned: 869 (million)
% 247.49/35.35 % TRYING [7]
% 247.49/35.35 % (3983730)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=936110755:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 247.49/35.35 % TRYING [8]
% 247.49/35.35 % (3983710)Instruction limit reached!
% 247.49/35.35 % (3983710)------------------------------
% 247.49/35.35 % (3983710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 247.49/35.35 % (3983710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.49/35.35 % (3983710)CaDiCaL version: 2.1.3
% 247.49/35.35 % (3983710)Termination reason: Instruction limit
% 247.49/35.35 % (3983710)Termination phase: Finite model building SAT solving
% 247.49/35.35 % (3983710)Time elapsed: 4.988 s
% 247.49/35.35 % (3983710)Peak memory usage: 183 MB
% 249.60/39.24 % (3983710)Instructions burned: 22067 (million)
% 249.60/39.24 % (3983733)dis+21_1_sil=32000:sas=cadical:random_seed=3753172402:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi)
% 249.60/39.24 % TRYING [9]
% 249.60/39.24 % (3983730)Instruction limit reached!
% 249.60/39.24 % (3983730)------------------------------
% 249.60/39.24 % (3983730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983730)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983730)Termination reason: Instruction limit
% 249.60/39.24 % (3983730)Termination phase: Saturation
% 249.60/39.24 % (3983730)Time elapsed: 1.829 s
% 249.60/39.24 % (3983730)Peak memory usage: 37 MB
% 249.60/39.24 % (3983730)Instructions burned: 3515 (million)
% 249.60/39.24 % (3983733)Instruction limit reached!
% 249.60/39.24 % (3983733)------------------------------
% 249.60/39.24 % (3983733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983733)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983733)Termination reason: Instruction limit
% 249.60/39.24 % (3983733)Termination phase: Saturation
% 249.60/39.24 % (3983733)Time elapsed: 1.089 s
% 249.60/39.24 % (3983733)Peak memory usage: 40 MB
% 249.60/39.24 % (3983733)Instructions burned: 3775 (million)
% 249.60/39.24 % (3983735)ott+11_1_sil=16000:gs=on:random_seed=3188182107:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi)
% 249.60/39.24 % (3983736)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=452667789:fmbsr=1.6:i=67534_2931 on theBenchmark for (2931ds/67534Mi)
% 249.60/39.24 % TRYING [7]
% 249.60/39.24 % TRYING [8]
% 249.60/39.24 % (3983726)Instruction limit reached!
% 249.60/39.24 % (3983726)------------------------------
% 249.60/39.24 % (3983726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983726)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983726)Termination reason: Instruction limit
% 249.60/39.24 % (3983726)Termination phase: Saturation
% 249.60/39.24 % (3983726)Time elapsed: 3.099 s
% 249.60/39.24 % (3983726)Peak memory usage: 45 MB
% 249.60/39.24 % (3983726)Instructions burned: 5114 (million)
% 249.60/39.24 % (3983739)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2311776383:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2924 on theBenchmark for (2924ds/4591Mi)
% 249.60/39.24 % TRYING [10]
% 249.60/39.24 % TRYING [11]
% 249.60/39.24 % (3983735)Instruction limit reached!
% 249.60/39.24 % (3983735)------------------------------
% 249.60/39.24 % (3983735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983735)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983735)Termination reason: Instruction limit
% 249.60/39.24 % (3983735)Termination phase: Saturation
% 249.60/39.24 % (3983735)Time elapsed: 1.362 s
% 249.60/39.24 % (3983735)Peak memory usage: 28 MB
% 249.60/39.24 % (3983735)Instructions burned: 2253 (million)
% 249.60/39.24 % (3983741)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3900943257:i=29340_2918 on theBenchmark for (2918ds/29340Mi)
% 249.60/39.24 % TRYING [9]
% 249.60/39.24 % (3983739)Instruction limit reached!
% 249.60/39.24 % (3983739)------------------------------
% 249.60/39.24 % (3983739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983739)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983739)Termination reason: Instruction limit
% 249.60/39.24 % (3983739)Termination phase: Saturation
% 249.60/39.24 % (3983739)Time elapsed: 1.878 s
% 249.60/39.24 % (3983739)Peak memory usage: 31 MB
% 249.60/39.24 % (3983739)Instructions burned: 4593 (million)
% 249.60/39.24 % (3983743)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1783189084:i=5211_2905 on theBenchmark for (2905ds/5211Mi)
% 249.60/39.24 % TRYING [10]
% 249.60/39.24 % (3983743)Instruction limit reached!
% 249.60/39.24 % (3983743)------------------------------
% 249.60/39.24 % (3983743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983743)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983743)Termination reason: Instruction limit
% 249.60/39.24 % (3983743)Termination phase: Saturation
% 249.60/39.24 % (3983743)Time elapsed: 2.898 s
% 249.60/39.24 % (3983743)Peak memory usage: 50 MB
% 249.60/39.24 % (3983743)Instructions burned: 5212 (million)
% 249.60/39.24 % (3983745)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3937340927:i=5497:nm=2_2876 on theBenchmark for (2876ds/5497Mi)
% 249.60/39.24 % TRYING [17]
% 249.60/39.24 % TRYING [11]
% 249.60/39.24 % (3983745)Instruction limit reached!
% 249.60/39.24 % (3983745)------------------------------
% 249.60/39.24 % (3983745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983745)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983745)Termination reason: Instruction limit
% 249.60/39.24 % (3983745)Termination phase: Finite model building constraint generation
% 249.60/39.24 % (3983745)Time elapsed: 1.997 s
% 249.60/39.24 % (3983745)Peak memory usage: 392 MB
% 249.60/39.24 % (3983745)Instructions burned: 5500 (million)
% 249.60/39.24 % (3983747)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3556601186:fmbsr=2:i=46332_2855 on theBenchmark for (2855ds/46332Mi)
% 249.60/39.24 % TRYING [15]
% 249.60/39.24 % TRYING [11]
% 249.60/39.24 % TRYING [12]
% 249.60/39.24 % (3983741)Instruction limit reached!
% 249.60/39.24 % (3983741)------------------------------
% 249.60/39.24 % (3983741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983741)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983741)Termination reason: Instruction limit
% 249.60/39.24 % (3983741)Termination phase: Saturation
% 249.60/39.24 % (3983741)Time elapsed: 16.566 s
% 249.60/39.24 % (3983741)Peak memory usage: 262 MB
% 249.60/39.24 % (3983741)Instructions burned: 29341 (million)
% 249.60/39.24 % (3983749)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3414233542:i=14071_2751 on theBenchmark for (2751ds/14071Mi)
% 249.60/39.24 % TRYING [12]
% 249.60/39.24 % (3983736)Instruction limit reached!
% 249.60/39.24 % (3983736)------------------------------
% 249.60/39.24 % (3983736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983736)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983736)Termination reason: Instruction limit
% 249.60/39.24 % (3983736)Termination phase: Finite model building SAT solving
% 249.60/39.24 % (3983736)Time elapsed: 19.554 s
% 249.60/39.24 % (3983736)Peak memory usage: 403 MB
% 249.60/39.24 % (3983736)Instructions burned: 67538 (million)
% 249.60/39.24 % (3983751)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=978766094:i=22565:add=on:rawr=on_2735 on theBenchmark for (2735ds/22565Mi)
% 249.60/39.24 % TRYING [12]
% 249.60/39.24 % (3983751)Instruction limit reached!
% 249.60/39.24 % (3983751)------------------------------
% 249.60/39.24 % (3983751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983751)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983751)Termination reason: Instruction limit
% 249.60/39.24 % (3983751)Termination phase: Saturation
% 249.60/39.24 % (3983751)Time elapsed: 5.620 s
% 249.60/39.24 % (3983751)Peak memory usage: 159 MB
% 249.60/39.24 % (3983751)Instructions burned: 22567 (million)
% 249.60/39.24 % (3983753)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1963345037:i=8173:av=off_2679 on theBenchmark for (2679ds/8173Mi)
% 249.60/39.24 % TRYING [12]
% 249.60/39.24 % (3983749)Instruction limit reached!
% 249.60/39.24 % (3983749)------------------------------
% 249.60/39.24 % (3983749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983749)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983749)Termination reason: Instruction limit
% 249.60/39.24 % (3983749)Termination phase: Finite model building SAT solving
% 249.60/39.24 % (3983749)Time elapsed: 9.156 s
% 249.60/39.24 % (3983749)Peak memory usage: 660 MB
% 249.60/39.24 % (3983749)Instructions burned: 14071 (million)
% 249.60/39.24 % (3983755)dis+10_16:1_sil=16000:random_seed=152711527:i=9155:fsr=off_2659 on theBenchmark for (2659ds/9155Mi)
% 249.60/39.24 % (3983753)Instruction limit reached!
% 249.60/39.24 % (3983753)------------------------------
% 249.60/39.24 % (3983753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.24 % (3983753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.24 % (3983753)CaDiCaL version: 2.1.3
% 249.60/39.24 % (3983753)Termination reason: Instruction limit
% 249.60/39.24 % (3983753)Termination phase: Saturation
% 249.60/39.24 % (3983753)Time elapsed: 2.884 s
% 249.60/39.24 % (3983753)Peak memory usage: 72 MB
% 249.60/39.24 % (3983753)Instructions burned: 8174 (million)
% 249.60/39.24 % (3983757)ott-3_8_sil=64000:random_seed=1731057054:i=20139:bs=on_2650 on theBenchmark for (2650ds/20139Mi)
% 249.60/39.24 % (3983757) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3983671-3983757"...
% 249.60/39.24 % (3983757)...printing done.
% 249.60/39.24 % (3983757)Refutation found. Thanks to Tanya!
% 249.60/39.24 % SZS status Theorem for theBenchmark
% 249.60/39.24 % SZS output start Proof for theBenchmark
% See solution above
% 249.60/39.25 % (3983757)------------------------------
% 249.60/39.25 % (3983757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 249.60/39.25 % (3983757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.60/39.25 % (3983757)CaDiCaL version: 2.1.3
% 249.60/39.25 % (3983757)Termination reason: Refutation
% 249.60/39.25 % (3983757)Time elapsed: 3.580 s
% 249.60/39.25 % (3983757)Peak memory usage: 79 MB
% 249.60/39.25 % (3983757)Instructions burned: 9838 (million)
% 249.60/39.25 % (3983671)Success in time 38.835 s
% 249.60/39.25 % Vampire exiting
%------------------------------------------------------------------------------