%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM008+2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:39:21 AM UTC 2026
% Result : Theorem 14.91s 2.84s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 13
% Syntax : Number of formulae : 98 ( 15 unt; 5 def)
% Number of atoms : 362 ( 25 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 515 ( 251 ~; 235 |; 18 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 7 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 144 ( 0 sgn 135 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ( transitive_reflexive_rewrite(b,X0)
& transitive_reflexive_rewrite(c,X0) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',found) ).
fof(f2,axiom,
( transitive_reflexive_rewrite(a,b)
& transitive_reflexive_rewrite(a,c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption) ).
fof(f3,axiom,
! [X0,X1] :
( X0 = X1
=> transitive_reflexive_rewrite(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equality_in_transitive_reflexive_rewrite) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( transitive_reflexive_rewrite(X0,X1)
& transitive_reflexive_rewrite(X1,X2) )
=> transitive_reflexive_rewrite(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_transitive_reflexive_rewrite) ).
fof(f6,axiom,
! [X0,X1,X2] :
( ( rewrite(X0,X1)
& rewrite(X0,X2) )
=> ? [X3] :
( transitive_reflexive_rewrite(X1,X3)
& transitive_reflexive_rewrite(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lo_cfl) ).
fof(f7,axiom,
! [X0,X1,X2] :
( ( rewrite(a,X0)
& transitive_reflexive_rewrite(X0,X1)
& transitive_reflexive_rewrite(X0,X2) )
=> ? [X3] :
( transitive_reflexive_rewrite(X1,X3)
& transitive_reflexive_rewrite(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ih_cfl) ).
fof(f8,axiom,
! [X0,X1] :
( transitive_reflexive_rewrite(X0,X1)
=> ( X0 = X1
| ? [X2] :
( rewrite(X0,X2)
& transitive_reflexive_rewrite(X2,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_or_rewrite) ).
fof(f9,conjecture,
goal,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_to_be_proved) ).
fof(f10,negated_conjecture,
~ goal,
inference(negated_conjecture,[status(cth)],[f9]) ).
fof(f11,plain,
~ goal,
inference(flattening,[],[f10]) ).
fof(f12,plain,
! [X0] :
( goal
| ~ transitive_reflexive_rewrite(b,X0)
| ~ transitive_reflexive_rewrite(c,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f13,plain,
! [X0] :
( goal
| ~ transitive_reflexive_rewrite(b,X0)
| ~ transitive_reflexive_rewrite(c,X0) ),
inference(flattening,[],[f12]) ).
fof(f14,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( rewrite(X0,X2)
& transitive_reflexive_rewrite(X2,X1) )
| ~ transitive_reflexive_rewrite(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f15,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( rewrite(X0,X2)
& transitive_reflexive_rewrite(X2,X1) )
| ~ transitive_reflexive_rewrite(X0,X1) ),
inference(flattening,[],[f14]) ).
fof(f16,plain,
! [X0,X1,X2] :
( ? [X3] :
( transitive_reflexive_rewrite(X1,X3)
& transitive_reflexive_rewrite(X2,X3) )
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f17,plain,
! [X0,X1,X2] :
( ? [X3] :
( transitive_reflexive_rewrite(X1,X3)
& transitive_reflexive_rewrite(X2,X3) )
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,X2) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0,X1,X2] :
( ? [X3] :
( transitive_reflexive_rewrite(X1,X3)
& transitive_reflexive_rewrite(X2,X3) )
| ~ rewrite(X0,X1)
| ~ rewrite(X0,X2) ),
inference(ennf_transformation,[],[f6]) ).
fof(f19,plain,
! [X0,X1,X2] :
( ? [X3] :
( transitive_reflexive_rewrite(X1,X3)
& transitive_reflexive_rewrite(X2,X3) )
| ~ rewrite(X0,X1)
| ~ rewrite(X0,X2) ),
inference(flattening,[],[f18]) ).
fof(f20,plain,
! [X0,X1,X2] :
( transitive_reflexive_rewrite(X0,X2)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X1,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f21,plain,
! [X0,X1,X2] :
( transitive_reflexive_rewrite(X0,X2)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X1,X2) ),
inference(flattening,[],[f20]) ).
fof(f23,plain,
! [X0,X1] :
( transitive_reflexive_rewrite(X0,X1)
| X0 != X1 ),
inference(ennf_transformation,[],[f3]) ).
fof(f24,plain,
! [X0,X1] :
( X0 = X1
| ( rewrite(X0,sK0(X0,X1))
& transitive_reflexive_rewrite(sK0(X0,X1),X1) )
| ~ transitive_reflexive_rewrite(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f15]) ).
fof(f25,plain,
! [X0,X1,X2] :
( ( transitive_reflexive_rewrite(X1,sK1(X1,X2))
& transitive_reflexive_rewrite(X2,sK1(X1,X2)) )
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X1,X2))],[f17]) ).
fof(f26,plain,
! [X0,X1,X2] :
( ( transitive_reflexive_rewrite(X1,sK2(X1,X2))
& transitive_reflexive_rewrite(X2,sK2(X1,X2)) )
| ~ rewrite(X0,X1)
| ~ rewrite(X0,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X1,X2))],[f19]) ).
fof(f27,plain,
~ goal,
inference(cnf_transformation,[],[f11]) ).
fof(f28,plain,
! [X0] :
( goal
| ~ transitive_reflexive_rewrite(b,X0)
| ~ transitive_reflexive_rewrite(c,X0) ),
inference(cnf_transformation,[],[f13]) ).
fof(f29,plain,
transitive_reflexive_rewrite(a,c),
inference(cnf_transformation,[],[f2]) ).
fof(f30,plain,
transitive_reflexive_rewrite(a,b),
inference(cnf_transformation,[],[f2]) ).
fof(f31,plain,
! [X0,X1] :
( transitive_reflexive_rewrite(sK0(X0,X1),X1)
| X0 = X1
| ~ transitive_reflexive_rewrite(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f32,plain,
! [X0,X1] :
( rewrite(X0,sK0(X0,X1))
| X0 = X1
| ~ transitive_reflexive_rewrite(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f33,plain,
! [X2,X0,X1] :
( transitive_reflexive_rewrite(X2,sK1(X1,X2))
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f34,plain,
! [X2,X0,X1] :
( transitive_reflexive_rewrite(X1,sK1(X1,X2))
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f35,plain,
! [X2,X0,X1] :
( transitive_reflexive_rewrite(X2,sK2(X1,X2))
| ~ rewrite(X0,X1)
| ~ rewrite(X0,X2) ),
inference(cnf_transformation,[],[f26]) ).
fof(f36,plain,
! [X2,X0,X1] :
( transitive_reflexive_rewrite(X1,sK2(X1,X2))
| ~ rewrite(X0,X1)
| ~ rewrite(X0,X2) ),
inference(cnf_transformation,[],[f26]) ).
fof(f37,plain,
! [X2,X0,X1] :
( transitive_reflexive_rewrite(X0,X2)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X1,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f39,plain,
! [X0,X1] :
( transitive_reflexive_rewrite(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f23]) ).
fof(f40,plain,
! [X1] : transitive_reflexive_rewrite(X1,X1),
inference(equality_resolution,[],[f39]) ).
fof(f42,definition,
( spl3_1
<=> ! [X0] :
( ~ transitive_reflexive_rewrite(b,X0)
| ~ transitive_reflexive_rewrite(c,X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f43,plain,
( ! [X0] :
( ~ transitive_reflexive_rewrite(c,X0)
| ~ transitive_reflexive_rewrite(b,X0) )
| ~ spl3_1 ),
inference(avatar_component_clause,[],[f42]) ).
fof(f45,definition,
( spl3_2
<=> goal ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f48,plain,
( spl3_1
| spl3_2 ),
inference(avatar_split_clause,[],[f28,f45,f42]) ).
fof(f49,plain,
~ spl3_2,
inference(avatar_split_clause,[],[f27,f45]) ).
fof(f65,plain,
( ! [X0,X1] :
( ~ transitive_reflexive_rewrite(c,X0)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(b,X1) )
| ~ spl3_1 ),
inference(resolution,[],[f37,f43]) ).
fof(f71,plain,
( ~ transitive_reflexive_rewrite(b,c)
| ~ spl3_1 ),
inference(resolution,[],[f40,f43]) ).
fof(f74,plain,
( ! [X2,X0,X1] :
( ~ transitive_reflexive_rewrite(sK1(X0,c),X1)
| ~ transitive_reflexive_rewrite(b,X1)
| ~ rewrite(a,X2)
| ~ transitive_reflexive_rewrite(X2,X0)
| ~ transitive_reflexive_rewrite(X2,c) )
| ~ spl3_1 ),
inference(resolution,[],[f65,f33]) ).
fof(f85,plain,
( ! [X2,X3,X0,X1] :
( ~ transitive_reflexive_rewrite(b,sK1(sK1(X0,c),X1))
| ~ rewrite(a,X2)
| ~ transitive_reflexive_rewrite(X2,X0)
| ~ transitive_reflexive_rewrite(X2,c)
| ~ rewrite(a,X3)
| ~ transitive_reflexive_rewrite(X3,sK1(X0,c))
| ~ transitive_reflexive_rewrite(X3,X1) )
| ~ spl3_1 ),
inference(resolution,[],[f74,f34]) ).
fof(f103,definition,
( spl3_5
<=> c = a ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f105,plain,
( c = a
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f116,plain,
( ! [X2,X3,X0,X1] :
( ~ transitive_reflexive_rewrite(X3,sK1(X1,c))
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(a,X2)
| ~ transitive_reflexive_rewrite(X2,sK1(X1,c))
| ~ transitive_reflexive_rewrite(X2,b)
| ~ rewrite(a,X3)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X3,b) )
| ~ spl3_1 ),
inference(resolution,[],[f85,f33]) ).
fof(f123,plain,
( ! [X2,X0,X1] :
( ~ transitive_reflexive_rewrite(X0,sK1(X1,c))
| ~ transitive_reflexive_rewrite(X2,X1)
| ~ transitive_reflexive_rewrite(X2,c)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,b)
| ~ rewrite(a,X0)
| ~ rewrite(a,X2)
| ~ transitive_reflexive_rewrite(X0,b) )
| ~ spl3_1 ),
inference(factoring,[],[f116]) ).
fof(f124,plain,
( ! [X2,X0,X1] :
( ~ transitive_reflexive_rewrite(X0,sK1(X1,c))
| ~ transitive_reflexive_rewrite(X2,X1)
| ~ transitive_reflexive_rewrite(X2,c)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,b)
| ~ rewrite(a,X2) )
| ~ spl3_1 ),
inference(duplicate_literal_removal,[],[f123]) ).
fof(f128,plain,
( ! [X2,X3,X0,X1] :
( ~ transitive_reflexive_rewrite(X3,sK1(X1,c))
| ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(a,X2)
| ~ transitive_reflexive_rewrite(X2,b)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X2,X3)
| ~ transitive_reflexive_rewrite(X0,X1) )
| ~ spl3_1 ),
inference(resolution,[],[f124,f37]) ).
fof(f154,definition,
( spl3_10
<=> b = a ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f155,plain,
( b != a
| spl3_10 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f156,plain,
( b = a
| ~ spl3_10 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f166,plain,
( ~ transitive_reflexive_rewrite(a,c)
| ~ spl3_1
| ~ spl3_10 ),
inference(superposition,[],[f71,f156]) ).
fof(f171,plain,
( $false
| ~ spl3_1
| ~ spl3_10 ),
inference(forward_subsumption_resolution,[],[f166,f29]) ).
fof(f172,plain,
( ~ spl3_1
| ~ spl3_10 ),
inference(avatar_contradiction_clause,[],[f171]) ).
fof(f301,plain,
( ! [X2,X3,X0,X1] :
( ~ rewrite(a,X3)
| ~ rewrite(a,X1)
| ~ transitive_reflexive_rewrite(X1,b)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X1,X2)
| ~ transitive_reflexive_rewrite(X0,X2)
| ~ transitive_reflexive_rewrite(X0,c)
| ~ transitive_reflexive_rewrite(X3,X2)
| ~ transitive_reflexive_rewrite(X3,c) )
| ~ spl3_1 ),
inference(resolution,[],[f128,f34]) ).
fof(f308,plain,
( ! [X2,X0,X1] :
( ~ rewrite(a,X0)
| ~ rewrite(a,X1)
| ~ transitive_reflexive_rewrite(X1,b)
| ~ transitive_reflexive_rewrite(X1,X2)
| ~ transitive_reflexive_rewrite(X0,X2)
| ~ transitive_reflexive_rewrite(X0,c)
| ~ transitive_reflexive_rewrite(X0,X2)
| ~ transitive_reflexive_rewrite(X0,c) )
| ~ spl3_1 ),
inference(factoring,[],[f301]) ).
fof(f309,plain,
( ! [X2,X0,X1] :
( ~ rewrite(a,X1)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X1,b)
| ~ transitive_reflexive_rewrite(X1,X2)
| ~ transitive_reflexive_rewrite(X0,X2)
| ~ transitive_reflexive_rewrite(X0,c) )
| ~ spl3_1 ),
inference(duplicate_literal_removal,[],[f308]) ).
fof(f311,plain,
( ! [X2,X0,X1] :
( ~ transitive_reflexive_rewrite(sK0(a,X1),b)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(sK0(a,X1),X2)
| ~ transitive_reflexive_rewrite(X0,X2)
| ~ transitive_reflexive_rewrite(X0,c)
| a = X1
| ~ transitive_reflexive_rewrite(a,X1) )
| ~ spl3_1 ),
inference(resolution,[],[f309,f32]) ).
fof(f314,plain,
( ! [X0,X1] :
( ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(sK0(a,b),X1)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,c)
| b = a
| ~ transitive_reflexive_rewrite(a,b)
| b = a
| ~ transitive_reflexive_rewrite(a,b) )
| ~ spl3_1 ),
inference(resolution,[],[f311,f31]) ).
fof(f319,plain,
( ! [X0,X1] :
( ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(sK0(a,b),X1)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,c)
| b = a
| ~ transitive_reflexive_rewrite(a,b) )
| ~ spl3_1 ),
inference(duplicate_literal_removal,[],[f314]) ).
fof(f320,plain,
( ! [X0,X1] :
( ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(sK0(a,b),X1)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,c)
| ~ transitive_reflexive_rewrite(a,b) )
| ~ spl3_1
| spl3_10 ),
inference(forward_subsumption_resolution,[],[f319,f155]) ).
fof(f321,plain,
( ! [X0,X1] :
( ~ transitive_reflexive_rewrite(sK0(a,b),X1)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,X1)
| ~ transitive_reflexive_rewrite(X0,c) )
| ~ spl3_1
| spl3_10 ),
inference(forward_subsumption_resolution,[],[f320,f30]) ).
fof(f328,plain,
( ! [X2,X0,X1] :
( ~ transitive_reflexive_rewrite(X0,sK2(sK0(a,b),X1))
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(X2,sK0(a,b))
| ~ rewrite(X2,X1) )
| ~ spl3_1
| spl3_10 ),
inference(resolution,[],[f321,f36]) ).
fof(f361,definition,
( spl3_16
<=> ! [X0] :
( ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(a,X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_16])],[avatar_definition]) ).
fof(f362,plain,
( ! [X0] :
( ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(X0,c) )
| ~ spl3_16 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f365,plain,
( ! [X2,X0,X1] :
( ~ rewrite(X2,sK0(a,b))
| ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(X1,sK0(a,b))
| ~ rewrite(X1,X0)
| ~ rewrite(a,X0)
| ~ rewrite(X2,X0) )
| ~ spl3_1
| spl3_10 ),
inference(resolution,[],[f328,f35]) ).
fof(f370,plain,
( ! [X0,X1] :
( ~ rewrite(X0,sK0(a,b))
| ~ transitive_reflexive_rewrite(X1,c)
| ~ rewrite(X0,X1)
| ~ rewrite(a,X1)
| ~ rewrite(X0,X1) )
| ~ spl3_1
| spl3_10 ),
inference(factoring,[],[f365]) ).
fof(f377,plain,
( ! [X0,X1] :
( ~ rewrite(X0,sK0(a,b))
| ~ transitive_reflexive_rewrite(X1,c)
| ~ rewrite(X0,X1)
| ~ rewrite(a,X1) )
| ~ spl3_1
| spl3_10 ),
inference(duplicate_literal_removal,[],[f370]) ).
fof(f379,plain,
( ! [X0] :
( ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(a,X0)
| ~ rewrite(a,X0)
| b = a
| ~ transitive_reflexive_rewrite(a,b) )
| ~ spl3_1
| spl3_10 ),
inference(resolution,[],[f377,f32]) ).
fof(f383,plain,
( ! [X0] :
( ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(a,X0)
| b = a
| ~ transitive_reflexive_rewrite(a,b) )
| ~ spl3_1
| spl3_10 ),
inference(duplicate_literal_removal,[],[f379]) ).
fof(f384,plain,
( ! [X0] :
( ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(a,X0)
| ~ transitive_reflexive_rewrite(a,b) )
| ~ spl3_1
| spl3_10 ),
inference(forward_subsumption_resolution,[],[f383,f155]) ).
fof(f385,plain,
( ! [X0] :
( ~ transitive_reflexive_rewrite(X0,c)
| ~ rewrite(a,X0) )
| ~ spl3_1
| spl3_10 ),
inference(forward_subsumption_resolution,[],[f384,f30]) ).
fof(f386,plain,
( spl3_16
| ~ spl3_1
| spl3_10 ),
inference(avatar_split_clause,[],[f385,f154,f42,f361]) ).
fof(f387,plain,
( ! [X0] :
( ~ transitive_reflexive_rewrite(sK0(a,X0),c)
| a = X0
| ~ transitive_reflexive_rewrite(a,X0) )
| ~ spl3_16 ),
inference(resolution,[],[f362,f32]) ).
fof(f388,plain,
( c = a
| ~ transitive_reflexive_rewrite(a,c)
| c = a
| ~ transitive_reflexive_rewrite(a,c)
| ~ spl3_16 ),
inference(resolution,[],[f387,f31]) ).
fof(f390,plain,
( c = a
| ~ transitive_reflexive_rewrite(a,c)
| ~ spl3_16 ),
inference(duplicate_literal_removal,[],[f388]) ).
fof(f391,plain,
( c = a
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f390,f29]) ).
fof(f392,plain,
( spl3_5
| ~ spl3_16 ),
inference(avatar_split_clause,[],[f391,f361,f103]) ).
fof(f394,plain,
( ! [X0] :
( ~ transitive_reflexive_rewrite(a,X0)
| ~ transitive_reflexive_rewrite(b,X0) )
| ~ spl3_1
| ~ spl3_5 ),
inference(superposition,[],[f43,f105]) ).
fof(f443,plain,
( ~ transitive_reflexive_rewrite(b,b)
| ~ spl3_1
| ~ spl3_5 ),
inference(resolution,[],[f394,f30]) ).
fof(f452,plain,
( $false
| ~ spl3_1
| ~ spl3_5 ),
inference(forward_subsumption_resolution,[],[f443,f40]) ).
fof(f453,plain,
( ~ spl3_1
| ~ spl3_5 ),
inference(avatar_contradiction_clause,[],[f452]) ).
cnf(s1,plain,
( spl3_1
| spl3_2 ),
inference(sat_conversion,[],[f48]) ).
cnf(s2,plain,
~ spl3_2,
inference(sat_conversion,[],[f49]) ).
cnf(s10,plain,
( ~ spl3_1
| ~ spl3_10 ),
inference(sat_conversion,[],[f172]) ).
cnf(s15,plain,
( ~ spl3_1
| spl3_10
| spl3_16 ),
inference(sat_conversion,[],[f386]) ).
cnf(s16,plain,
( spl3_5
| ~ spl3_16 ),
inference(sat_conversion,[],[f392]) ).
cnf(s18,plain,
( ~ spl3_1
| ~ spl3_5 ),
inference(sat_conversion,[],[f453]) ).
cnf(s19,plain,
spl3_1,
inference(rat,[],[s1,s2]) ).
cnf(s20,plain,
~ spl3_5,
inference(rat,[],[s18,s19]) ).
cnf(s21,plain,
~ spl3_10,
inference(rat,[],[s10,s19]) ).
cnf(s24,plain,
~ spl3_16,
inference(rat,[],[s16,s20]) ).
cnf(s25,plain,
$false,
inference(rat,[],[s15,s19,s24,s21]) ).
fof(f454,plain,
$false,
inference(avatar_sat_refutation,[],[s25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM008+2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 21:49:03 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 12.97/2.52 % (4063717)Detected formulas, will run a generic FOF schedule.
% 12.97/2.52 % (4063833)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1461708910:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.97/2.52 % (4063830)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2608615579:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.97/2.52 % (4063829)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=1167328248:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.97/2.52 % (4063832)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=79637045:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.97/2.52 % (4063827)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=1466620005:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.97/2.52 % (4063828)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=532922862:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.97/2.52 % (4063835)dis-21_1_sil=8000:lcm=predicate:random_seed=1455082202: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)
% 12.97/2.52 % (4063830)Refutation not found, incomplete strategy
% 12.97/2.52 % (4063830)------------------------------
% 12.97/2.52 % (4063830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.52 % (4063830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.52 % (4063830)CaDiCaL version: 2.1.3
% 12.97/2.52 % (4063830)Termination reason: Refutation not found, incomplete strategy
% 12.97/2.52 % (4063830)Time elapsed: 0.001 s
% 12.97/2.52 % (4063830)Peak memory usage: 86 MB
% 12.97/2.52 % (4063833)Instruction limit reached!
% 12.97/2.52 % (4063833)------------------------------
% 12.97/2.52 % (4063833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.52 % (4063833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.52 % (4063833)CaDiCaL version: 2.1.3
% 12.97/2.52 % (4063833)Termination reason: Instruction limit
% 12.97/2.52 % (4063833)Termination phase: Saturation
% 12.97/2.52 % (4063833)Time elapsed: 0.073 s
% 12.97/2.52 % (4063833)Peak memory usage: 89 MB
% 12.97/2.52 % (4063833)Instructions burned: 139 (million)
% 12.97/2.52 % (4063832)Instruction limit reached!
% 12.97/2.52 % (4063832)------------------------------
% 12.97/2.52 % (4063832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.52 % (4063832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.52 % (4063832)CaDiCaL version: 2.1.3
% 12.97/2.52 % (4063832)Termination reason: Instruction limit
% 12.97/2.52 % (4063832)Termination phase: Saturation
% 12.97/2.52 % (4063832)Time elapsed: 0.060 s
% 12.97/2.52 % (4063832)Peak memory usage: 87 MB
% 12.97/2.52 % (4063832)Instructions burned: 120 (million)
% 12.97/2.52 % (4063835)Instruction limit reached!
% 12.97/2.52 % (4063835)------------------------------
% 12.97/2.52 % (4063835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.52 % (4063835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.52 % (4063835)CaDiCaL version: 2.1.3
% 12.97/2.52 % (4063835)Termination reason: Instruction limit
% 12.97/2.52 % (4063835)Termination phase: Saturation
% 12.97/2.52 % (4063835)Time elapsed: 0.073 s
% 12.97/2.52 % (4063835)Peak memory usage: 88 MB
% 12.97/2.52 % (4063835)Instructions burned: 130 (million)
% 12.97/2.52 % (4063880)lrs+10_1_sil=8000:sp=occurrence:random_seed=2173840672:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.97/2.52 % (4063882)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3896740708:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.97/2.52 % (4063882)Refutation not found, incomplete strategy
% 12.97/2.52 % (4063882)------------------------------
% 12.97/2.52 % (4063882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.52 % (4063882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.52 % (4063882)CaDiCaL version: 2.1.3
% 12.97/2.52 % (4063882)Termination reason: Refutation not found, incomplete strategy
% 12.97/2.52 % (4063882)Time elapsed: 0.001 s
% 14.91/2.84 % (4063882)Peak memory usage: 87 MB
% 14.91/2.84 % (4063883)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1780464609:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 14.91/2.84 % (4063883)Refutation not found, incomplete strategy
% 14.91/2.84 % (4063883)------------------------------
% 14.91/2.84 % (4063883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4063883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4063883)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4063883)Termination reason: Refutation not found, incomplete strategy
% 14.91/2.84 % (4063883)Time elapsed: 0.001 s
% 14.91/2.84 % (4063883)Peak memory usage: 87 MB
% 14.91/2.84 % (4063830)------------------------------
% 14.91/2.84 % (4063830)------------------------------
% 14.91/2.84 % (4063880)Instruction limit reached!
% 14.91/2.84 % (4063880)------------------------------
% 14.91/2.84 % (4063880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4063880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4063880)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4063880)Termination reason: Instruction limit
% 14.91/2.84 % (4063880)Termination phase: Saturation
% 14.91/2.84 % (4063880)Time elapsed: 0.092 s
% 14.91/2.84 % (4063880)Peak memory usage: 92 MB
% 14.91/2.84 % (4063880)Instructions burned: 286 (million)
% 14.91/2.84 % (4063925)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2355809067:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 14.91/2.84 % (4063925)Refutation not found, incomplete strategy
% 14.91/2.84 % (4063925)------------------------------
% 14.91/2.84 % (4063925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4063925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4063925)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4063925)Termination reason: Refutation not found, incomplete strategy
% 14.91/2.84 % (4063925)Time elapsed: 0.001 s
% 14.91/2.84 % (4063925)Peak memory usage: 88 MB
% 14.91/2.84 % (4063922)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=166663258:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 14.91/2.84 % (4063882)------------------------------
% 14.91/2.84 % (4063882)------------------------------
% 14.91/2.84 % (4063883)------------------------------
% 14.91/2.84 % (4063883)------------------------------
% 14.91/2.84 % (4063925)------------------------------
% 14.91/2.84 % (4063925)------------------------------
% 14.91/2.84 % (4063922)Instruction limit reached!
% 14.91/2.84 % (4063922)------------------------------
% 14.91/2.84 % (4063922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4063922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4063922)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4063922)Termination reason: Instruction limit
% 14.91/2.84 % (4063922)Termination phase: Saturation
% 14.91/2.84 % (4063922)Time elapsed: 0.139 s
% 14.91/2.84 % (4063922)Peak memory usage: 91 MB
% 14.91/2.84 % (4063922)Instructions burned: 248 (million)
% 14.91/2.84 % (4063938)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2970760797:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 14.91/2.84 % (4063949)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=678542788:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 14.91/2.84 % (4063966)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2458590581:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 14.91/2.84 % (4063973)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2951891898:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 14.91/2.84 % (4063973)Refutation not found, incomplete strategy
% 14.91/2.84 % (4063973)------------------------------
% 14.91/2.84 % (4063973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4063973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4063973)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4063973)Termination reason: Refutation not found, incomplete strategy
% 14.91/2.84 % (4063973)Time elapsed: 0.001 s
% 14.91/2.84 % (4063973)Peak memory usage: 87 MB
% 14.91/2.84 % (4063949)Instruction limit reached!
% 14.91/2.84 % (4063949)------------------------------
% 14.91/2.84 % (4063949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4063949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4063949)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4063949)Termination reason: Instruction limit
% 14.91/2.84 % (4063949)Termination phase: Saturation
% 14.91/2.84 % (4063949)Time elapsed: 0.074 s
% 14.91/2.84 % (4063949)Peak memory usage: 89 MB
% 14.91/2.84 % (4063949)Instructions burned: 113 (million)
% 14.91/2.84 % (4063966)Instruction limit reached!
% 14.91/2.84 % (4063966)------------------------------
% 14.91/2.84 % (4063966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4063966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4063966)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4063966)Termination reason: Instruction limit
% 14.91/2.84 % (4063966)Termination phase: Saturation
% 14.91/2.84 % (4063966)Time elapsed: 0.069 s
% 14.91/2.84 % (4063966)Peak memory usage: 88 MB
% 14.91/2.84 % (4063966)Instructions burned: 129 (million)
% 14.91/2.84 % (4064004)lrs+10_1_sil=8000:sp=occurrence:random_seed=3963108724:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 14.91/2.84 % (4064005)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=517981348:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 14.91/2.84 % (4064005)Refutation not found, incomplete strategy
% 14.91/2.84 % (4064005)------------------------------
% 14.91/2.84 % (4064005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4064005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4064005)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4064005)Termination reason: Refutation not found, incomplete strategy
% 14.91/2.84 % (4064005)Time elapsed: 0.001 s
% 14.91/2.84 % (4064005)Peak memory usage: 88 MB
% 14.91/2.84 % (4063973)------------------------------
% 14.91/2.84 % (4063973)------------------------------
% 14.91/2.84 % (4064055)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1191160794:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 14.91/2.84 % (4064005)------------------------------
% 14.91/2.84 % (4064005)------------------------------
% 14.91/2.84 % (4064057)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2805669152:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 14.91/2.84 % (4064057)Refutation not found, incomplete strategy
% 14.91/2.84 % (4064057)------------------------------
% 14.91/2.84 % (4064057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4064057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4064057)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4064057)Termination reason: Refutation not found, incomplete strategy
% 14.91/2.84 % (4064057)Time elapsed: 0.002 s
% 14.91/2.84 % (4064057)Peak memory usage: 88 MB
% 14.91/2.84 % (4064057)Instructions burned: 1 (million)
% 14.91/2.84 % (4064004)Instruction limit reached!
% 14.91/2.84 % (4064004)------------------------------
% 14.91/2.84 % (4064004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4064004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4064004)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4064004)Termination reason: Instruction limit
% 14.91/2.84 % (4064004)Termination phase: Saturation
% 14.91/2.84 % (4064004)Time elapsed: 0.540 s
% 14.91/2.84 % (4064004)Peak memory usage: 95 MB
% 14.91/2.84 % (4064004)Instructions burned: 907 (million)
% 14.91/2.84 % (4064057)------------------------------
% 14.91/2.84 % (4064057)------------------------------
% 14.91/2.84 % (4064059)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3412013251:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 14.91/2.84 % (4064059)Refutation not found, incomplete strategy
% 14.91/2.84 % (4064059)------------------------------
% 14.91/2.84 % (4064059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4064059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4064059)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4064059)Termination reason: Refutation not found, incomplete strategy
% 14.91/2.84 % (4064059)Time elapsed: 0.001 s
% 14.91/2.84 % (4064059)Peak memory usage: 88 MB
% 14.91/2.84 % (4064060)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3337483572:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 14.91/2.84 % (4064055)First to succeed.
% 14.91/2.84 % (4064055)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4063717"
% 14.91/2.84 % (4064059)------------------------------
% 14.91/2.84 % (4064059)------------------------------
% 14.91/2.84 % (4064063)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=2620300010:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 14.91/2.84 % (4064063)Refutation not found, incomplete strategy
% 14.91/2.84 % (4064063)------------------------------
% 14.91/2.84 % (4064063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/2.84 % (4064063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/2.84 % (4064063)CaDiCaL version: 2.1.3
% 14.91/2.84 % (4064063)Termination reason: Refutation not found, incomplete strategy
% 14.91/2.84 % (4064063)Time elapsed: 0.002 s
% 14.91/2.84 % (4064063)Peak memory usage: 88 MB
% 14.91/2.84 % (4064063)Instructions burned: 1 (million)
% 14.91/2.84 % (4064055)Refutation found. Thanks to Tanya!
% 14.91/2.84 % SZS status Theorem for theBenchmark
% 14.91/2.84 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/3.03 % (4064055)------------------------------
% 0.20/3.03 % (4064055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/3.03 % (4064055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.03 % (4064055)CaDiCaL version: 2.1.3
% 0.20/3.03 % (4064055)Termination reason: Refutation
% 0.20/3.03 % (4064055)Time elapsed: 0.672 s
% 0.20/3.03 % (4064055)Peak memory usage: 129 MB
% 0.20/3.03 % (4064055)Instructions burned: 1002 (million)
% 0.20/3.03 % (4064055)------------------------------
% 0.20/3.03 % (4064055)------------------------------
% 0.20/3.03 % (4063717)Success in time 2.17 s
% 0.20/3.03 % Vampire exiting
%------------------------------------------------------------------------------