%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HAL002+1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 10:18:52 AM UTC 2026
% Result : Theorem 1.61s 1.66s
% Output : Refutation 5.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 26
% Syntax : Number of formulae : 189 ( 12 unt; 15 def)
% Number of atoms : 605 ( 105 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 718 ( 302 ~; 352 |; 31 &)
% ( 17 <=>; 15 =>; 0 <=; 1 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 16 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 199 ( 0 sgn 193 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( morphism(X0,X1,X2)
=> ( ! [X3] :
( element(X3,X1)
=> element(apply(X0,X3),X2) )
& apply(X0,zero(X1)) = zero(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',morphism) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( injection(X0)
& morphism(X0,X1,X2) )
=> ! [X3,X4] :
( ( element(X3,X1)
& element(X4,X1)
& apply(X0,X3) = apply(X0,X4) )
=> X3 = X4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',injection_properties) ).
fof(f3,axiom,
! [X0,X1,X2] :
( ( morphism(X0,X1,X2)
& ! [X3,X4] :
( ( element(X3,X1)
& element(X4,X1)
& apply(X0,X3) = apply(X0,X4) )
=> X3 = X4 ) )
=> injection(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',properties_for_injection) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( element(X1,X0)
& element(X2,X0) )
=> element(subtract(X0,X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subtract_in_domain) ).
fof(f11,axiom,
! [X0,X1] :
( element(X1,X0)
=> subtract(X0,X1,X1) = zero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subtract_to_0) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( element(X1,X0)
& element(X2,X0) )
=> subtract(X0,X1,subtract(X0,X1,X2)) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subtract_cancellation) ).
fof(f13,axiom,
! [X0,X1,X2] :
( morphism(X0,X1,X2)
=> ! [X3,X4] :
( ( element(X3,X1)
& element(X4,X1) )
=> apply(X0,subtract(X1,X3,X4)) = subtract(X2,apply(X0,X3),apply(X0,X4)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subtract_distribution) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( injection_2(X0)
& morphism(X0,X1,X2) )
=> ! [X3] :
( ( element(X3,X1)
& apply(X0,X3) = zero(X2) )
=> X3 = zero(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',injection_properties_2) ).
fof(f15,axiom,
! [X0,X1,X2] :
( ( morphism(X0,X1,X2)
& ! [X3] :
( ( element(X3,X1)
& apply(X0,X3) = zero(X2) )
=> X3 = zero(X1) ) )
=> injection_2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',properties_for_injection_2) ).
fof(f16,axiom,
morphism(x,any1,any2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_morphism) ).
fof(f17,conjecture,
( injection(x)
<=> injection_2(x) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',my) ).
fof(f18,negated_conjecture,
~ ( injection(x)
<=> injection_2(x) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
! [X0,X1,X2] :
( ( ! [X3] :
( element(apply(X0,X3),X2)
| ~ element(X3,X1) )
& apply(X0,zero(X1)) = zero(X2) )
| ~ morphism(X0,X1,X2) ),
inference(ennf_transformation,[],[f1]) ).
fof(f20,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( X3 = X4
| ~ element(X3,X1)
| ~ element(X4,X1)
| apply(X0,X3) != apply(X0,X4) )
| ~ injection(X0)
| ~ morphism(X0,X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f21,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( X3 = X4
| ~ element(X3,X1)
| ~ element(X4,X1)
| apply(X0,X3) != apply(X0,X4) )
| ~ injection(X0)
| ~ morphism(X0,X1,X2) ),
inference(flattening,[],[f20]) ).
fof(f22,plain,
! [X0,X1,X2] :
( injection(X0)
| ~ morphism(X0,X1,X2)
| ? [X3,X4] :
( X3 != X4
& element(X3,X1)
& element(X4,X1)
& apply(X0,X3) = apply(X0,X4) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f23,plain,
! [X0,X1,X2] :
( injection(X0)
| ~ morphism(X0,X1,X2)
| ? [X3,X4] :
( X3 != X4
& element(X3,X1)
& element(X4,X1)
& apply(X0,X3) = apply(X0,X4) ) ),
inference(flattening,[],[f22]) ).
fof(f36,plain,
! [X0,X1,X2] :
( element(subtract(X0,X1,X2),X0)
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f37,plain,
! [X0,X1,X2] :
( element(subtract(X0,X1,X2),X0)
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(flattening,[],[f36]) ).
fof(f38,plain,
! [X0,X1] :
( subtract(X0,X1,X1) = zero(X0)
| ~ element(X1,X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f39,plain,
! [X0,X1,X2] :
( subtract(X0,X1,subtract(X0,X1,X2)) = X2
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f40,plain,
! [X0,X1,X2] :
( subtract(X0,X1,subtract(X0,X1,X2)) = X2
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(flattening,[],[f39]) ).
fof(f41,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( apply(X0,subtract(X1,X3,X4)) = subtract(X2,apply(X0,X3),apply(X0,X4))
| ~ element(X3,X1)
| ~ element(X4,X1) )
| ~ morphism(X0,X1,X2) ),
inference(ennf_transformation,[],[f13]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( apply(X0,subtract(X1,X3,X4)) = subtract(X2,apply(X0,X3),apply(X0,X4))
| ~ element(X3,X1)
| ~ element(X4,X1) )
| ~ morphism(X0,X1,X2) ),
inference(flattening,[],[f41]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ! [X3] :
( X3 = zero(X1)
| ~ element(X3,X1)
| apply(X0,X3) != zero(X2) )
| ~ injection_2(X0)
| ~ morphism(X0,X1,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ! [X3] :
( X3 = zero(X1)
| ~ element(X3,X1)
| apply(X0,X3) != zero(X2) )
| ~ injection_2(X0)
| ~ morphism(X0,X1,X2) ),
inference(flattening,[],[f43]) ).
fof(f45,plain,
! [X0,X1,X2] :
( injection_2(X0)
| ~ morphism(X0,X1,X2)
| ? [X3] :
( zero(X1) != X3
& element(X3,X1)
& apply(X0,X3) = zero(X2) ) ),
inference(ennf_transformation,[],[f15]) ).
fof(f46,plain,
! [X0,X1,X2] :
( injection_2(X0)
| ~ morphism(X0,X1,X2)
| ? [X3] :
( zero(X1) != X3
& element(X3,X1)
& apply(X0,X3) = zero(X2) ) ),
inference(flattening,[],[f45]) ).
fof(f47,plain,
( injection(x)
<~> injection_2(x) ),
inference(ennf_transformation,[],[f18]) ).
fof(f48,plain,
! [X0,X1,X2] :
( injection(X0)
| ~ morphism(X0,X1,X2)
| ( sK0(X0,X1) != sK1(X0,X1)
& element(sK0(X0,X1),X1)
& element(sK1(X0,X1),X1)
& apply(X0,sK0(X0,X1)) = apply(X0,sK1(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X3,sK0(X0,X1)),skolemize(X4,sK1(X0,X1))],[f23]) ).
fof(f60,plain,
! [X0,X1,X2] :
( injection_2(X0)
| ~ morphism(X0,X1,X2)
| ( zero(X1) != sK8(X0,X1,X2)
& element(sK8(X0,X1,X2),X1)
& zero(X2) = apply(X0,sK8(X0,X1,X2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f46]) ).
fof(f61,plain,
( ( ~ injection_2(x)
| ~ injection(x) )
& ( injection_2(x)
| injection(x) ) ),
inference(nnf_transformation,[],[f47]) ).
fof(f63,plain,
! [X2,X3,X0,X1] :
( element(apply(X0,X3),X2)
| ~ element(X3,X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[],[f19]) ).
fof(f64,plain,
! [X2,X3,X0,X1,X4] :
( ~ injection(X0)
| ~ element(X3,X1)
| ~ element(X4,X1)
| apply(X0,X3) != apply(X0,X4)
| X3 = X4
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f65,plain,
! [X2,X0,X1] :
( injection(X0)
| ~ morphism(X0,X1,X2)
| apply(X0,sK0(X0,X1)) = apply(X0,sK1(X0,X1)) ),
inference(cnf_transformation,[],[f48]) ).
fof(f66,plain,
! [X2,X0,X1] :
( element(sK1(X0,X1),X1)
| ~ morphism(X0,X1,X2)
| injection(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f67,plain,
! [X2,X0,X1] :
( element(sK0(X0,X1),X1)
| ~ morphism(X0,X1,X2)
| injection(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f68,plain,
! [X2,X0,X1] :
( sK0(X0,X1) != sK1(X0,X1)
| ~ morphism(X0,X1,X2)
| injection(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f85,plain,
! [X2,X0,X1] :
( element(subtract(X0,X1,X2),X0)
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(cnf_transformation,[],[f37]) ).
fof(f86,plain,
! [X0,X1] :
( subtract(X0,X1,X1) = zero(X0)
| ~ element(X1,X0) ),
inference(cnf_transformation,[],[f38]) ).
fof(f87,plain,
! [X2,X0,X1] :
( subtract(X0,X1,subtract(X0,X1,X2)) = X2
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f88,plain,
! [X2,X3,X0,X1,X4] :
( ~ morphism(X0,X1,X2)
| ~ element(X3,X1)
| ~ element(X4,X1)
| apply(X0,subtract(X1,X3,X4)) = subtract(X2,apply(X0,X3),apply(X0,X4)) ),
inference(cnf_transformation,[],[f42]) ).
fof(f89,plain,
! [X2,X3,X0,X1] :
( ~ morphism(X0,X1,X2)
| ~ element(X3,X1)
| apply(X0,X3) != zero(X2)
| ~ injection_2(X0)
| zero(X1) = X3 ),
inference(cnf_transformation,[],[f44]) ).
fof(f90,plain,
! [X2,X0,X1] :
( injection_2(X0)
| ~ morphism(X0,X1,X2)
| zero(X2) = apply(X0,sK8(X0,X1,X2)) ),
inference(cnf_transformation,[],[f60]) ).
fof(f91,plain,
! [X2,X0,X1] :
( injection_2(X0)
| ~ morphism(X0,X1,X2)
| element(sK8(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f60]) ).
fof(f92,plain,
! [X2,X0,X1] :
( zero(X1) != sK8(X0,X1,X2)
| ~ morphism(X0,X1,X2)
| injection_2(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f93,plain,
morphism(x,any1,any2),
inference(cnf_transformation,[],[f16]) ).
fof(f94,plain,
( injection_2(x)
| injection(x) ),
inference(cnf_transformation,[],[f61]) ).
fof(f95,plain,
( ~ injection_2(x)
| ~ injection(x) ),
inference(cnf_transformation,[],[f61]) ).
fof(f99,definition,
( spl9_1
<=> injection(x) ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
fof(f100,plain,
( ~ injection(x)
| spl9_1 ),
inference(avatar_component_clause,[],[f99]) ).
fof(f101,plain,
( injection(x)
| ~ spl9_1 ),
inference(avatar_component_clause,[],[f99]) ).
fof(f103,definition,
( spl9_2
<=> injection_2(x) ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f104,plain,
( ~ injection_2(x)
| spl9_2 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f106,plain,
( spl9_1
| spl9_2 ),
inference(avatar_split_clause,[],[f94,f103,f99]) ).
fof(f107,plain,
( ~ spl9_1
| ~ spl9_2 ),
inference(avatar_split_clause,[],[f95,f103,f99]) ).
fof(f112,plain,
! [X0,X1] :
( element(zero(X0),X0)
| ~ element(X1,X0)
| ~ element(X1,X0)
| ~ element(X1,X0) ),
inference(superposition,[],[f85,f86]) ).
fof(f113,plain,
! [X0,X1] :
( element(zero(X0),X0)
| ~ element(X1,X0) ),
inference(duplicate_literal_removal,[],[f112]) ).
fof(f115,plain,
( ! [X0,X1] :
( ~ morphism(x,X0,X1)
| apply(x,sK0(x,X0)) = apply(x,sK1(x,X0)) )
| spl9_1 ),
inference(resolution,[],[f65,f100]) ).
fof(f116,plain,
( apply(x,sK0(x,any1)) = apply(x,sK1(x,any1))
| spl9_1 ),
inference(resolution,[],[f115,f93]) ).
fof(f117,plain,
! [X0] :
( ~ element(X0,any1)
| apply(x,X0) != zero(any2)
| ~ injection_2(x)
| zero(any1) = X0 ),
inference(resolution,[],[f89,f93]) ).
fof(f128,definition,
( spl9_4
<=> element(sK1(x,any1),any1) ),
introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition]) ).
fof(f129,plain,
( element(sK1(x,any1),any1)
| ~ spl9_4 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f130,plain,
( ~ element(sK1(x,any1),any1)
| spl9_4 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f136,plain,
( ! [X0] :
( ~ morphism(x,any1,X0)
| injection(x) )
| spl9_4 ),
inference(resolution,[],[f130,f66]) ).
fof(f137,plain,
( ! [X0] : ~ morphism(x,any1,X0)
| spl9_1
| spl9_4 ),
inference(forward_subsumption_resolution,[],[f136,f100]) ).
fof(f138,plain,
! [X0,X1] :
( subtract(X0,X1,zero(X0)) = X1
| ~ element(X1,X0)
| ~ element(X1,X0)
| ~ element(X1,X0) ),
inference(superposition,[],[f87,f86]) ).
fof(f141,plain,
! [X0,X1] :
( subtract(X0,X1,zero(X0)) = X1
| ~ element(X1,X0) ),
inference(duplicate_literal_removal,[],[f138]) ).
fof(f142,plain,
( $false
| spl9_1
| spl9_4 ),
inference(resolution,[],[f137,f93]) ).
fof(f143,plain,
( spl9_1
| spl9_4 ),
inference(avatar_contradiction_clause,[],[f142]) ).
fof(f147,plain,
! [X0,X1] :
( apply(x,subtract(any1,X0,X1)) = subtract(any2,apply(x,X0),apply(x,X1))
| ~ element(X1,any1)
| ~ element(X0,any1) ),
inference(resolution,[],[f88,f93]) ).
fof(f202,plain,
( ! [X0] :
( apply(x,subtract(any1,X0,sK1(x,any1))) = subtract(any2,apply(x,X0),apply(x,sK0(x,any1)))
| ~ element(sK1(x,any1),any1)
| ~ element(X0,any1) )
| spl9_1 ),
inference(superposition,[],[f147,f116]) ).
fof(f208,plain,
! [X0] :
( zero(any2) = apply(x,subtract(any1,X0,X0))
| ~ element(apply(x,X0),any2)
| ~ element(X0,any1)
| ~ element(X0,any1) ),
inference(superposition,[],[f86,f147]) ).
fof(f211,plain,
! [X0] :
( ~ element(apply(x,X0),any2)
| zero(any2) = apply(x,subtract(any1,X0,X0))
| ~ element(X0,any1) ),
inference(duplicate_literal_removal,[],[f208]) ).
fof(f216,plain,
( ! [X0] :
( apply(x,subtract(any1,X0,sK1(x,any1))) = subtract(any2,apply(x,X0),apply(x,sK0(x,any1)))
| ~ element(X0,any1) )
| spl9_1
| ~ spl9_4 ),
inference(forward_subsumption_resolution,[],[f202,f129]) ).
fof(f223,plain,
( zero(any2) = apply(x,subtract(any1,sK0(x,any1),sK1(x,any1)))
| ~ element(sK0(x,any1),any1)
| ~ element(apply(x,sK0(x,any1)),any2)
| spl9_1
| ~ spl9_4 ),
inference(superposition,[],[f216,f86]) ).
fof(f231,definition,
( spl9_8
<=> element(apply(x,sK0(x,any1)),any2) ),
introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition]) ).
fof(f233,plain,
( ~ element(apply(x,sK0(x,any1)),any2)
| spl9_8 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f243,definition,
( spl9_11
<=> element(sK0(x,any1),any1) ),
introduced(definition,[new_symbols(definition,[spl9_11])],[avatar_definition]) ).
fof(f244,plain,
( element(sK0(x,any1),any1)
| ~ spl9_11 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f245,plain,
( ~ element(sK0(x,any1),any1)
| spl9_11 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl9_12
<=> zero(any2) = apply(x,subtract(any1,sK0(x,any1),sK1(x,any1))) ),
introduced(definition,[new_symbols(definition,[spl9_12])],[avatar_definition]) ).
fof(f249,plain,
( zero(any2) = apply(x,subtract(any1,sK0(x,any1),sK1(x,any1)))
| ~ spl9_12 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f255,plain,
( ~ spl9_8
| ~ spl9_11
| spl9_12
| spl9_1
| ~ spl9_4 ),
inference(avatar_split_clause,[],[f223,f128,f99,f247,f243,f231]) ).
fof(f310,plain,
( ! [X0] :
( ~ morphism(x,any1,X0)
| injection(x) )
| spl9_11 ),
inference(resolution,[],[f245,f67]) ).
fof(f311,plain,
( ! [X0] : ~ morphism(x,any1,X0)
| spl9_1
| spl9_11 ),
inference(forward_subsumption_resolution,[],[f310,f100]) ).
fof(f312,plain,
( $false
| spl9_1
| spl9_11 ),
inference(resolution,[],[f311,f93]) ).
fof(f313,plain,
( spl9_1
| spl9_11 ),
inference(avatar_contradiction_clause,[],[f312]) ).
fof(f360,plain,
( ! [X0] :
( ~ morphism(x,X0,any2)
| ~ element(sK0(x,any1),X0) )
| spl9_8 ),
inference(resolution,[],[f233,f63]) ).
fof(f365,definition,
( spl9_24
<=> ! [X0] :
( ~ element(X0,any1)
| zero(any1) = X0
| apply(x,X0) != zero(any2) ) ),
introduced(definition,[new_symbols(definition,[spl9_24])],[avatar_definition]) ).
fof(f366,plain,
( ! [X0] :
( apply(x,X0) != zero(any2)
| zero(any1) = X0
| ~ element(X0,any1) )
| ~ spl9_24 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f367,plain,
( ~ spl9_2
| spl9_24 ),
inference(avatar_split_clause,[],[f117,f365,f103]) ).
fof(f372,definition,
( spl9_26
<=> ! [X0,X1] :
( ~ element(X0,any1)
| ~ element(X1,any1)
| X0 = X1
| apply(x,X0) != apply(x,X1) ) ),
introduced(definition,[new_symbols(definition,[spl9_26])],[avatar_definition]) ).
fof(f373,plain,
( ! [X0,X1] :
( apply(x,X0) != apply(x,X1)
| ~ element(X1,any1)
| X0 = X1
| ~ element(X0,any1) )
| ~ spl9_26 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f380,plain,
( ! [X2,X3,X0,X1] :
( ~ morphism(x,X1,X3)
| ~ element(X2,X1)
| apply(x,X0) != apply(x,X2)
| X0 = X2
| ~ element(X0,X1) )
| ~ spl9_1 ),
inference(resolution,[],[f101,f64]) ).
fof(f381,plain,
( ! [X0,X1] :
( ~ morphism(x,X0,X1)
| zero(X1) = apply(x,sK8(x,X0,X1)) )
| spl9_2 ),
inference(resolution,[],[f104,f90]) ).
fof(f382,plain,
( ! [X0,X1] :
( element(sK8(x,X0,X1),X0)
| ~ morphism(x,X0,X1) )
| spl9_2 ),
inference(resolution,[],[f104,f91]) ).
fof(f383,plain,
( ~ element(sK0(x,any1),any1)
| spl9_8 ),
inference(resolution,[],[f360,f93]) ).
fof(f386,plain,
( ~ spl9_11
| spl9_8 ),
inference(avatar_split_clause,[],[f383,f231,f243]) ).
fof(f387,plain,
( zero(any2) = apply(x,sK8(x,any1,any2))
| spl9_2 ),
inference(resolution,[],[f381,f93]) ).
fof(f389,plain,
( ! [X0,X1] :
( ~ element(X0,any1)
| apply(x,X0) != apply(x,X1)
| X0 = X1
| ~ element(X1,any1) )
| ~ spl9_1 ),
inference(resolution,[],[f380,f93]) ).
fof(f390,plain,
( spl9_26
| ~ spl9_1 ),
inference(avatar_split_clause,[],[f389,f99,f372]) ).
fof(f393,plain,
( ! [X0,X1] :
( element(zero(any2),X0)
| ~ element(sK8(x,any1,any2),X1)
| ~ morphism(x,X1,X0) )
| spl9_2 ),
inference(superposition,[],[f63,f387]) ).
fof(f395,definition,
( spl9_28
<=> element(sK8(x,any1,any2),any1) ),
introduced(definition,[new_symbols(definition,[spl9_28])],[avatar_definition]) ).
fof(f396,plain,
( element(sK8(x,any1,any2),any1)
| ~ spl9_28 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f397,plain,
( ~ element(sK8(x,any1,any2),any1)
| spl9_28 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f408,plain,
( ~ morphism(x,any1,any2)
| spl9_2
| spl9_28 ),
inference(resolution,[],[f397,f382]) ).
fof(f409,plain,
( $false
| spl9_2
| spl9_28 ),
inference(forward_subsumption_resolution,[],[f408,f93]) ).
fof(f410,plain,
( spl9_2
| spl9_28 ),
inference(avatar_contradiction_clause,[],[f409]) ).
fof(f411,plain,
( ! [X0] :
( apply(x,X0) != zero(any2)
| ~ element(X0,any1)
| sK8(x,any1,any2) = X0
| ~ element(sK8(x,any1,any2),any1) )
| spl9_2
| ~ spl9_26 ),
inference(superposition,[],[f373,f387]) ).
fof(f418,definition,
( spl9_31
<=> ! [X0] :
( apply(x,X0) != zero(any2)
| ~ element(X0,any1)
| sK8(x,any1,any2) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl9_31])],[avatar_definition]) ).
fof(f419,plain,
( ! [X0] :
( apply(x,X0) != zero(any2)
| ~ element(X0,any1)
| sK8(x,any1,any2) = X0 )
| ~ spl9_31 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f421,plain,
( ~ spl9_28
| spl9_31
| spl9_2
| ~ spl9_26 ),
inference(avatar_split_clause,[],[f411,f372,f103,f418,f395]) ).
fof(f448,definition,
( spl9_32
<=> element(zero(any2),any2) ),
introduced(definition,[new_symbols(definition,[spl9_32])],[avatar_definition]) ).
fof(f449,plain,
( element(zero(any2),any2)
| ~ spl9_32 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f450,plain,
( ~ element(zero(any2),any2)
| spl9_32 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f472,plain,
( ! [X0] :
( ~ morphism(x,X0,any2)
| ~ element(sK8(x,any1,any2),X0) )
| spl9_2
| spl9_32 ),
inference(resolution,[],[f450,f393]) ).
fof(f486,plain,
( ~ element(sK8(x,any1,any2),any1)
| spl9_2
| spl9_32 ),
inference(resolution,[],[f472,f93]) ).
fof(f487,plain,
( $false
| spl9_2
| ~ spl9_28
| spl9_32 ),
inference(forward_subsumption_resolution,[],[f486,f396]) ).
fof(f488,plain,
( spl9_2
| ~ spl9_28
| spl9_32 ),
inference(avatar_contradiction_clause,[],[f487]) ).
fof(f506,plain,
( ~ element(zero(any2),any2)
| zero(any2) = apply(x,subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2)))
| ~ element(sK8(x,any1,any2),any1)
| spl9_2 ),
inference(superposition,[],[f211,f387]) ).
fof(f511,plain,
( zero(any2) = apply(x,subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2)))
| ~ element(sK8(x,any1,any2),any1)
| spl9_2
| ~ spl9_32 ),
inference(forward_subsumption_resolution,[],[f506,f449]) ).
fof(f512,plain,
( zero(any2) = apply(x,subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2)))
| spl9_2
| ~ spl9_28
| ~ spl9_32 ),
inference(forward_subsumption_resolution,[],[f511,f396]) ).
fof(f519,plain,
( zero(any2) != zero(any2)
| ~ element(subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2)),any1)
| sK8(x,any1,any2) = subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2))
| spl9_2
| ~ spl9_28
| ~ spl9_31
| ~ spl9_32 ),
inference(superposition,[],[f419,f512]) ).
fof(f525,plain,
( ~ element(subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2)),any1)
| sK8(x,any1,any2) = subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2))
| spl9_2
| ~ spl9_28
| ~ spl9_31
| ~ spl9_32 ),
inference(trivial_inequality_removal,[],[f519]) ).
fof(f527,definition,
( spl9_33
<=> element(subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2)),any1) ),
introduced(definition,[new_symbols(definition,[spl9_33])],[avatar_definition]) ).
fof(f529,plain,
( ~ element(subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2)),any1)
| spl9_33 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f544,definition,
( spl9_37
<=> sK8(x,any1,any2) = subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2)) ),
introduced(definition,[new_symbols(definition,[spl9_37])],[avatar_definition]) ).
fof(f546,plain,
( sK8(x,any1,any2) = subtract(any1,sK8(x,any1,any2),sK8(x,any1,any2))
| ~ spl9_37 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f547,plain,
( spl9_37
| ~ spl9_33
| spl9_2
| ~ spl9_28
| ~ spl9_31
| ~ spl9_32 ),
inference(avatar_split_clause,[],[f525,f448,f418,f395,f103,f527,f544]) ).
fof(f565,plain,
( ~ element(zero(any1),any1)
| ~ element(sK8(x,any1,any2),any1)
| spl9_33 ),
inference(superposition,[],[f529,f86]) ).
fof(f567,plain,
( ~ element(sK8(x,any1,any2),any1)
| spl9_33 ),
inference(forward_subsumption_resolution,[],[f565,f113]) ).
fof(f570,plain,
( $false
| ~ spl9_28
| spl9_33 ),
inference(forward_subsumption_resolution,[],[f567,f396]) ).
fof(f571,plain,
( ~ spl9_28
| spl9_33 ),
inference(avatar_contradiction_clause,[],[f570]) ).
fof(f578,plain,
( zero(any1) = sK8(x,any1,any2)
| ~ element(sK8(x,any1,any2),any1)
| ~ spl9_37 ),
inference(superposition,[],[f86,f546]) ).
fof(f583,plain,
( zero(any1) = sK8(x,any1,any2)
| ~ spl9_28
| ~ spl9_37 ),
inference(forward_subsumption_resolution,[],[f578,f396]) ).
fof(f597,plain,
( zero(any1) != zero(any1)
| ~ morphism(x,any1,any2)
| injection_2(x)
| ~ spl9_28
| ~ spl9_37 ),
inference(superposition,[],[f92,f583]) ).
fof(f598,plain,
( ~ morphism(x,any1,any2)
| injection_2(x)
| ~ spl9_28
| ~ spl9_37 ),
inference(trivial_inequality_removal,[],[f597]) ).
fof(f599,plain,
( injection_2(x)
| ~ spl9_28
| ~ spl9_37 ),
inference(forward_subsumption_resolution,[],[f598,f93]) ).
fof(f601,plain,
( $false
| spl9_2
| ~ spl9_28
| ~ spl9_37 ),
inference(forward_subsumption_resolution,[],[f599,f104]) ).
fof(f602,plain,
( spl9_2
| ~ spl9_28
| ~ spl9_37 ),
inference(avatar_contradiction_clause,[],[f601]) ).
fof(f621,plain,
( zero(any2) != zero(any2)
| zero(any1) = subtract(any1,sK0(x,any1),sK1(x,any1))
| ~ element(subtract(any1,sK0(x,any1),sK1(x,any1)),any1)
| ~ spl9_12
| ~ spl9_24 ),
inference(superposition,[],[f366,f249]) ).
fof(f627,plain,
( zero(any1) = subtract(any1,sK0(x,any1),sK1(x,any1))
| ~ element(subtract(any1,sK0(x,any1),sK1(x,any1)),any1)
| ~ spl9_12
| ~ spl9_24 ),
inference(trivial_inequality_removal,[],[f621]) ).
fof(f633,definition,
( spl9_41
<=> element(subtract(any1,sK0(x,any1),sK1(x,any1)),any1) ),
introduced(definition,[new_symbols(definition,[spl9_41])],[avatar_definition]) ).
fof(f635,plain,
( ~ element(subtract(any1,sK0(x,any1),sK1(x,any1)),any1)
| spl9_41 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f643,definition,
( spl9_43
<=> zero(any1) = subtract(any1,sK0(x,any1),sK1(x,any1)) ),
introduced(definition,[new_symbols(definition,[spl9_43])],[avatar_definition]) ).
fof(f645,plain,
( zero(any1) = subtract(any1,sK0(x,any1),sK1(x,any1))
| ~ spl9_43 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f646,plain,
( ~ spl9_41
| spl9_43
| ~ spl9_12
| ~ spl9_24 ),
inference(avatar_split_clause,[],[f627,f365,f247,f643,f633]) ).
fof(f661,plain,
( ~ element(sK0(x,any1),any1)
| ~ element(sK1(x,any1),any1)
| spl9_41 ),
inference(resolution,[],[f635,f85]) ).
fof(f662,plain,
( ~ element(sK1(x,any1),any1)
| ~ spl9_11
| spl9_41 ),
inference(forward_subsumption_resolution,[],[f661,f244]) ).
fof(f663,plain,
( $false
| ~ spl9_4
| ~ spl9_11
| spl9_41 ),
inference(forward_subsumption_resolution,[],[f662,f129]) ).
fof(f664,plain,
( ~ spl9_4
| ~ spl9_11
| spl9_41 ),
inference(avatar_contradiction_clause,[],[f663]) ).
fof(f685,plain,
( sK1(x,any1) = subtract(any1,sK0(x,any1),zero(any1))
| ~ element(sK0(x,any1),any1)
| ~ element(sK1(x,any1),any1)
| ~ spl9_43 ),
inference(superposition,[],[f87,f645]) ).
fof(f687,plain,
( sK1(x,any1) = subtract(any1,sK0(x,any1),zero(any1))
| ~ element(sK1(x,any1),any1)
| ~ spl9_11
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f685,f244]) ).
fof(f689,plain,
( sK1(x,any1) = subtract(any1,sK0(x,any1),zero(any1))
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f687,f129]) ).
fof(f693,plain,
( sK0(x,any1) = sK1(x,any1)
| ~ element(sK0(x,any1),any1)
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(superposition,[],[f141,f689]) ).
fof(f696,plain,
( sK0(x,any1) = sK1(x,any1)
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f693,f244]) ).
fof(f704,plain,
( ! [X0] :
( sK0(x,any1) != sK0(x,any1)
| ~ morphism(x,any1,X0)
| injection(x) )
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(superposition,[],[f68,f696]) ).
fof(f706,plain,
( ! [X0] :
( ~ morphism(x,any1,X0)
| injection(x) )
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(trivial_inequality_removal,[],[f704]) ).
fof(f707,plain,
( ! [X0] : ~ morphism(x,any1,X0)
| spl9_1
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f706,f100]) ).
fof(f713,plain,
( $false
| spl9_1
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(resolution,[],[f707,f93]) ).
fof(f714,plain,
( spl9_1
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(avatar_contradiction_clause,[],[f713]) ).
cnf(s1,plain,
( spl9_1
| spl9_2 ),
inference(sat_conversion,[],[f106]) ).
cnf(s2,plain,
( ~ spl9_1
| ~ spl9_2 ),
inference(sat_conversion,[],[f107]) ).
cnf(s4,plain,
( spl9_1
| spl9_4 ),
inference(sat_conversion,[],[f143]) ).
cnf(s10,plain,
( spl9_1
| ~ spl9_4
| ~ spl9_8
| ~ spl9_11
| spl9_12 ),
inference(sat_conversion,[],[f255]) ).
cnf(s18,plain,
( spl9_1
| spl9_11 ),
inference(sat_conversion,[],[f313]) ).
cnf(s26,plain,
( ~ spl9_2
| spl9_24 ),
inference(sat_conversion,[],[f367]) ).
cnf(s30,plain,
( spl9_8
| ~ spl9_11 ),
inference(sat_conversion,[],[f386]) ).
cnf(s31,plain,
( ~ spl9_1
| spl9_26 ),
inference(sat_conversion,[],[f390]) ).
cnf(s35,plain,
( spl9_2
| spl9_28 ),
inference(sat_conversion,[],[f410]) ).
cnf(s37,plain,
( spl9_2
| ~ spl9_26
| ~ spl9_28
| spl9_31 ),
inference(sat_conversion,[],[f421]) ).
cnf(s44,plain,
( spl9_2
| ~ spl9_28
| spl9_32 ),
inference(sat_conversion,[],[f488]) ).
cnf(s52,plain,
( spl9_2
| ~ spl9_28
| ~ spl9_31
| ~ spl9_32
| ~ spl9_33
| spl9_37 ),
inference(sat_conversion,[],[f547]) ).
cnf(s56,plain,
( ~ spl9_28
| spl9_33 ),
inference(sat_conversion,[],[f571]) ).
cnf(s58,plain,
( spl9_2
| ~ spl9_28
| ~ spl9_37 ),
inference(sat_conversion,[],[f602]) ).
cnf(s63,plain,
( ~ spl9_12
| ~ spl9_24
| ~ spl9_41
| spl9_43 ),
inference(sat_conversion,[],[f646]) ).
cnf(s67,plain,
( ~ spl9_4
| ~ spl9_11
| spl9_41 ),
inference(sat_conversion,[],[f664]) ).
cnf(s71,plain,
( spl9_1
| ~ spl9_4
| ~ spl9_11
| ~ spl9_43 ),
inference(sat_conversion,[],[f714]) ).
cnf(s72,plain,
spl9_1,
inference(rat,[],[s63,s10,s26,s67,s71,s30,s1,s4,s18]) ).
cnf(s73,plain,
spl9_26,
inference(rat,[],[s31,s72]) ).
cnf(s74,plain,
~ spl9_2,
inference(rat,[],[s2,s72]) ).
cnf(s75,plain,
spl9_28,
inference(rat,[],[s35,s74]) ).
cnf(s76,plain,
~ spl9_37,
inference(rat,[],[s58,s74,s75]) ).
cnf(s77,plain,
spl9_33,
inference(rat,[],[s56,s75]) ).
cnf(s78,plain,
spl9_32,
inference(rat,[],[s44,s74,s75]) ).
cnf(s81,plain,
spl9_31,
inference(rat,[],[s37,s74,s73,s75]) ).
cnf(s84,plain,
$false,
inference(rat,[],[s52,s76,s77,s78,s74,s75,s81]) ).
fof(f715,plain,
$false,
inference(avatar_sat_refutation,[],[s84]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : HAL002+1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.46 % Computer : n026.cluster.edu
% 0.17/0.46 % Model : x86_64 x86_64
% 0.17/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.46 % Memory : 8046.5625MB
% 0.17/0.46 % OS : Linux 6.8.0-71-generic
% 0.17/0.46 % CPULimit : 300
% 0.17/0.46 % WCLimit : 300
% 0.17/0.46 % DateTime : Sun Sep 27 10:51:26 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.17/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.51 Running first-order theorem proving
% 0.21/0.51 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.61/1.66 % (2656103)Detected formulas, will run a generic FOF schedule.
% 1.61/1.66 % (2656114)dis-21_1_sil=8000:lcm=predicate:random_seed=1100621372: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)
% 1.61/1.66 % (2656108)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=1071564938:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.61/1.66 % (2656114)Instruction limit reached!
% 1.61/1.66 % (2656114)------------------------------
% 1.61/1.66 % (2656114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.61/1.66 % (2656114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.61/1.66 % (2656114)CaDiCaL version: 2.1.3
% 1.61/1.66 % (2656114)Termination reason: Instruction limit
% 1.61/1.66 % (2656114)Termination phase: Saturation
% 1.61/1.66 % (2656114)Time elapsed: 0.053 s
% 1.61/1.66 % (2656114)Peak memory usage: 89 MB
% 1.61/1.66 % (2656114)Instructions burned: 130 (million)
% 1.61/1.66 % (2656111)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1315140824:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.61/1.66 % (2656109)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=1858661477:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.61/1.66 % (2656110)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=3738246392:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.61/1.66 % (2656111)Refutation not found, incomplete strategy
% 1.61/1.66 % (2656111)------------------------------
% 1.61/1.66 % (2656111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.61/1.66 % (2656111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.61/1.66 % (2656111)CaDiCaL version: 2.1.3
% 1.61/1.66 % (2656111)Termination reason: Refutation not found, incomplete strategy
% 1.61/1.66 % (2656111)Time elapsed: 0.003 s
% 1.61/1.66 % (2656111)Peak memory usage: 88 MB
% 1.61/1.66 % (2656111)Instructions burned: 1 (million)
% 1.61/1.66 % (2656112)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3791028891:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.61/1.66 % (2656113)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2102365601:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.61/1.66 % (2656113)First to succeed.
% 1.61/1.66 % (2656113)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2656103"
% 1.61/1.66 % (2656112)Instruction limit reached!
% 1.61/1.66 % (2656112)------------------------------
% 1.61/1.66 % (2656112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.61/1.66 % (2656112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.61/1.66 % (2656112)CaDiCaL version: 2.1.3
% 1.61/1.66 % (2656112)Termination reason: Instruction limit
% 1.61/1.66 % (2656112)Termination phase: Saturation
% 1.61/1.66 % (2656112)Time elapsed: 0.096 s
% 1.61/1.66 % (2656112)Peak memory usage: 88 MB
% 1.61/1.66 % (2656112)Instructions burned: 119 (million)
% 1.61/1.66 % (2656120)lrs+10_1_sil=8000:sp=occurrence:random_seed=324380603:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 1.61/1.66 % (2656120)Instruction limit reached!
% 1.61/1.66 % (2656120)------------------------------
% 1.61/1.66 % (2656120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.61/1.66 % (2656120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.61/1.66 % (2656120)CaDiCaL version: 2.1.3
% 1.61/1.66 % (2656120)Termination reason: Instruction limit
% 1.61/1.66 % (2656120)Termination phase: Saturation
% 1.61/1.66 % (2656120)Time elapsed: 0.155 s
% 1.61/1.66 % (2656120)Peak memory usage: 92 MB
% 1.61/1.66 % (2656120)Instructions burned: 286 (million)
% 1.61/1.66 % (2656123)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2883336304:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 1.61/1.66 % (2656123)Refutation not found, incomplete strategy
% 1.61/1.66 % (2656123)------------------------------
% 1.61/1.66 % (2656123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.61/1.66 % (2656123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.61/1.66 % (2656123)CaDiCaL version: 2.1.3
% 1.61/1.66 % (2656123)Termination reason: Refutation not found, incomplete strategy
% 1.61/1.66 % (2656123)Time elapsed: 0.004 s
% 1.61/1.66 % (2656123)Peak memory usage: 89 MB
% 1.61/1.66 % (2656123)Instructions burned: 2 (million)
% 1.61/1.66 % (2656111)------------------------------
% 1.61/1.66 % (2656111)------------------------------
% 1.61/1.66 % (2656113)Refutation found. Thanks to Tanya!
% 1.61/1.66 % SZS status Theorem for theBenchmark
% 1.61/1.66 % SZS output start Proof for theBenchmark
% See solution above
% 5.04/1.81 % (2656113)------------------------------
% 5.04/1.81 % (2656113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.04/1.81 % (2656113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.04/1.81 % (2656113)CaDiCaL version: 2.1.3
% 5.04/1.81 % (2656113)Termination reason: Refutation
% 5.04/1.81 % (2656113)Time elapsed: 0.034 s
% 5.04/1.81 % (2656113)Peak memory usage: 90 MB
% 5.04/1.81 % (2656113)Instructions burned: 34 (million)
% 5.04/1.81 % (2656113)------------------------------
% 5.04/1.81 % (2656113)------------------------------
% 5.04/1.81 % (2656103)Success in time 0.599 s
% 5.04/1.81 % Vampire exiting
%------------------------------------------------------------------------------