%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU261+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 12:52:38 PM UTC 2026
% Result : Theorem 1.12s 0.64s
% Output : Refutation 1.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 9
% Syntax : Number of formulae : 104 ( 24 unt; 6 def)
% Number of atoms : 379 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 477 ( 202 ~; 212 |; 37 &)
% ( 8 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 7 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 59 ( 0 sgn 53 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f51,axiom,
! [X0] :
( relation(X0)
=> ( well_ordering(X0)
<=> ( reflexive(X0)
& transitive(X0)
& antisymmetric(X0)
& connected(X0)
& well_founded_relation(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_wellord1) ).
fof(f280,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( relation_isomorphism(X0,X1,X2)
=> ( ( reflexive(X0)
=> reflexive(X1) )
& ( transitive(X0)
=> transitive(X1) )
& ( connected(X0)
=> connected(X1) )
& ( antisymmetric(X0)
=> antisymmetric(X1) )
& ( well_founded_relation(X0)
=> well_founded_relation(X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t53_wellord1) ).
fof(f283,conjecture,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( ( well_ordering(X0)
& relation_isomorphism(X0,X1,X2) )
=> well_ordering(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_wellord1) ).
fof(f284,negated_conjecture,
~ ! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( ( well_ordering(X0)
& relation_isomorphism(X0,X1,X2) )
=> well_ordering(X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f283]) ).
fof(f377,plain,
! [X0] :
( ( well_ordering(X0)
<=> ( reflexive(X0)
& transitive(X0)
& antisymmetric(X0)
& connected(X0)
& well_founded_relation(X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f595,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( reflexive(X1)
| ~ reflexive(X0) )
& ( transitive(X1)
| ~ transitive(X0) )
& ( connected(X1)
| ~ connected(X0) )
& ( antisymmetric(X1)
| ~ antisymmetric(X0) )
& ( well_founded_relation(X1)
| ~ well_founded_relation(X0) ) )
| ~ relation_isomorphism(X0,X1,X2)
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f280]) ).
fof(f596,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( reflexive(X1)
| ~ reflexive(X0) )
& ( transitive(X1)
| ~ transitive(X0) )
& ( connected(X1)
| ~ connected(X0) )
& ( antisymmetric(X1)
| ~ antisymmetric(X0) )
& ( well_founded_relation(X1)
| ~ well_founded_relation(X0) ) )
| ~ relation_isomorphism(X0,X1,X2)
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(flattening,[],[f595]) ).
fof(f601,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ well_ordering(X1)
& well_ordering(X0)
& relation_isomorphism(X0,X1,X2)
& relation(X2)
& function(X2) )
& relation(X1) )
& relation(X0) ),
inference(ennf_transformation,[],[f284]) ).
fof(f602,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ well_ordering(X1)
& well_ordering(X0)
& relation_isomorphism(X0,X1,X2)
& relation(X2)
& function(X2) )
& relation(X1) )
& relation(X0) ),
inference(flattening,[],[f601]) ).
fof(f836,plain,
! [X0] :
( ~ well_ordering(X0)
| well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f377]) ).
fof(f837,plain,
! [X0] :
( ~ well_ordering(X0)
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f377]) ).
fof(f838,plain,
! [X0] :
( antisymmetric(X0)
| ~ relation(X0)
| ~ well_ordering(X0) ),
inference(cnf_transformation,[],[f377]) ).
fof(f839,plain,
! [X0] :
( transitive(X0)
| ~ relation(X0)
| ~ well_ordering(X0) ),
inference(cnf_transformation,[],[f377]) ).
fof(f840,plain,
! [X0] :
( reflexive(X0)
| ~ relation(X0)
| ~ well_ordering(X0) ),
inference(cnf_transformation,[],[f377]) ).
fof(f841,plain,
! [X0] :
( ~ well_founded_relation(X0)
| ~ relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ),
inference(cnf_transformation,[],[f377]) ).
fof(f1228,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ reflexive(X0)
| reflexive(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1229,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ transitive(X0)
| transitive(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1230,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ connected(X0)
| connected(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1231,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ antisymmetric(X0)
| antisymmetric(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1232,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| ~ relation(X1)
| ~ function(X2)
| ~ relation(X2)
| ~ relation_isomorphism(X0,X1,X2)
| ~ well_founded_relation(X0)
| well_founded_relation(X1) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1244,plain,
function(sK118),
inference(cnf_transformation,[],[f602]) ).
fof(f1245,plain,
relation(sK118),
inference(cnf_transformation,[],[f602]) ).
fof(f1246,plain,
relation_isomorphism(sK116,sK117,sK118),
inference(cnf_transformation,[],[f602]) ).
fof(f1247,plain,
well_ordering(sK116),
inference(cnf_transformation,[],[f602]) ).
fof(f1248,plain,
~ well_ordering(sK117),
inference(cnf_transformation,[],[f602]) ).
fof(f1249,plain,
relation(sK117),
inference(cnf_transformation,[],[f602]) ).
fof(f1250,plain,
relation(sK116),
inference(cnf_transformation,[],[f602]) ).
fof(f1801,plain,
! [X2,X0,X1] :
( ~ relation_isomorphism(X0,X1,X2)
| ~ relation(X1)
| function(X2)
| ~ relation(X2)
| ~ relation(X0)
| ~ well_founded_relation(X0)
| well_founded_relation(X1) ),
inference(consistent_polarity_flipping,[],[f1232]) ).
fof(f1802,plain,
! [X2,X0,X1] :
( ~ relation_isomorphism(X0,X1,X2)
| ~ relation(X1)
| function(X2)
| ~ relation(X2)
| ~ relation(X0)
| ~ antisymmetric(X0)
| antisymmetric(X1) ),
inference(consistent_polarity_flipping,[],[f1231]) ).
fof(f1803,plain,
! [X2,X0,X1] :
( ~ relation_isomorphism(X0,X1,X2)
| ~ relation(X1)
| function(X2)
| ~ relation(X2)
| ~ relation(X0)
| ~ connected(X0)
| connected(X1) ),
inference(consistent_polarity_flipping,[],[f1230]) ).
fof(f1804,plain,
! [X2,X0,X1] :
( ~ relation_isomorphism(X0,X1,X2)
| ~ relation(X1)
| function(X2)
| ~ relation(X2)
| ~ relation(X0)
| ~ transitive(X0)
| transitive(X1) ),
inference(consistent_polarity_flipping,[],[f1229]) ).
fof(f1805,plain,
! [X2,X0,X1] :
( ~ relation_isomorphism(X0,X1,X2)
| ~ relation(X1)
| function(X2)
| ~ relation(X2)
| ~ relation(X0)
| ~ reflexive(X0)
| reflexive(X1) ),
inference(consistent_polarity_flipping,[],[f1228]) ).
fof(f1816,plain,
~ function(sK118),
inference(consistent_polarity_flipping,[],[f1244]) ).
fof(f1931,plain,
( well_founded_relation(sK116)
| ~ relation(sK116) ),
inference(resolution,[],[f836,f1247]) ).
fof(f1932,plain,
well_founded_relation(sK116),
inference(forward_subsumption_resolution,[],[f1931,f1250]) ).
fof(f1933,plain,
( connected(sK116)
| ~ relation(sK116) ),
inference(resolution,[],[f837,f1247]) ).
fof(f1934,plain,
connected(sK116),
inference(forward_subsumption_resolution,[],[f1933,f1250]) ).
fof(f6866,plain,
( ~ relation(sK117)
| function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ well_founded_relation(sK116)
| well_founded_relation(sK117) ),
inference(resolution,[],[f1801,f1246]) ).
fof(f6867,plain,
( function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ well_founded_relation(sK116)
| well_founded_relation(sK117) ),
inference(forward_subsumption_resolution,[],[f6866,f1249]) ).
fof(f6868,plain,
( ~ relation(sK118)
| ~ relation(sK116)
| ~ well_founded_relation(sK116)
| well_founded_relation(sK117) ),
inference(forward_subsumption_resolution,[],[f6867,f1816]) ).
fof(f6869,plain,
( ~ relation(sK116)
| ~ well_founded_relation(sK116)
| well_founded_relation(sK117) ),
inference(forward_subsumption_resolution,[],[f6868,f1245]) ).
fof(f6870,plain,
( ~ well_founded_relation(sK116)
| well_founded_relation(sK117) ),
inference(forward_subsumption_resolution,[],[f6869,f1250]) ).
fof(f6871,plain,
well_founded_relation(sK117),
inference(forward_subsumption_resolution,[],[f6870,f1932]) ).
fof(f6872,plain,
( ~ relation(sK117)
| ~ connected(sK117)
| ~ antisymmetric(sK117)
| ~ transitive(sK117)
| ~ reflexive(sK117)
| well_ordering(sK117) ),
inference(resolution,[],[f6871,f841]) ).
fof(f6873,plain,
( ~ connected(sK117)
| ~ antisymmetric(sK117)
| ~ transitive(sK117)
| ~ reflexive(sK117)
| well_ordering(sK117) ),
inference(forward_subsumption_resolution,[],[f6872,f1249]) ).
fof(f6874,plain,
( ~ connected(sK117)
| ~ antisymmetric(sK117)
| ~ transitive(sK117)
| ~ reflexive(sK117) ),
inference(forward_subsumption_resolution,[],[f6873,f1248]) ).
fof(f6876,definition,
( spl125_97
<=> reflexive(sK117) ),
introduced(definition,[new_symbols(definition,[spl125_97])],[avatar_definition]) ).
fof(f6878,plain,
( ~ reflexive(sK117)
| spl125_97 ),
inference(avatar_component_clause,[],[f6876]) ).
fof(f6880,definition,
( spl125_98
<=> transitive(sK117) ),
introduced(definition,[new_symbols(definition,[spl125_98])],[avatar_definition]) ).
fof(f6884,definition,
( spl125_99
<=> antisymmetric(sK117) ),
introduced(definition,[new_symbols(definition,[spl125_99])],[avatar_definition]) ).
fof(f6888,definition,
( spl125_100
<=> connected(sK117) ),
introduced(definition,[new_symbols(definition,[spl125_100])],[avatar_definition]) ).
fof(f6891,plain,
( ~ spl125_97
| ~ spl125_98
| ~ spl125_99
| ~ spl125_100 ),
inference(avatar_split_clause,[],[f6874,f6888,f6884,f6880,f6876]) ).
fof(f6893,plain,
( ~ relation(sK117)
| function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ antisymmetric(sK116)
| antisymmetric(sK117) ),
inference(resolution,[],[f1802,f1246]) ).
fof(f6894,plain,
( function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ antisymmetric(sK116)
| antisymmetric(sK117) ),
inference(forward_subsumption_resolution,[],[f6893,f1249]) ).
fof(f6895,plain,
( ~ relation(sK118)
| ~ relation(sK116)
| ~ antisymmetric(sK116)
| antisymmetric(sK117) ),
inference(forward_subsumption_resolution,[],[f6894,f1816]) ).
fof(f6896,plain,
( ~ relation(sK116)
| ~ antisymmetric(sK116)
| antisymmetric(sK117) ),
inference(forward_subsumption_resolution,[],[f6895,f1245]) ).
fof(f6897,plain,
( ~ antisymmetric(sK116)
| antisymmetric(sK117) ),
inference(forward_subsumption_resolution,[],[f6896,f1250]) ).
fof(f6899,definition,
( spl125_101
<=> antisymmetric(sK116) ),
introduced(definition,[new_symbols(definition,[spl125_101])],[avatar_definition]) ).
fof(f6901,plain,
( ~ antisymmetric(sK116)
| spl125_101 ),
inference(avatar_component_clause,[],[f6899]) ).
fof(f6902,plain,
( spl125_99
| ~ spl125_101 ),
inference(avatar_split_clause,[],[f6897,f6899,f6884]) ).
fof(f6903,plain,
( ~ relation(sK117)
| function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ connected(sK116)
| connected(sK117) ),
inference(resolution,[],[f1803,f1246]) ).
fof(f6904,plain,
( function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ connected(sK116)
| connected(sK117) ),
inference(forward_subsumption_resolution,[],[f6903,f1249]) ).
fof(f6905,plain,
( ~ relation(sK118)
| ~ relation(sK116)
| ~ connected(sK116)
| connected(sK117) ),
inference(forward_subsumption_resolution,[],[f6904,f1816]) ).
fof(f6906,plain,
( ~ relation(sK116)
| ~ connected(sK116)
| connected(sK117) ),
inference(forward_subsumption_resolution,[],[f6905,f1245]) ).
fof(f6907,plain,
( ~ connected(sK116)
| connected(sK117) ),
inference(forward_subsumption_resolution,[],[f6906,f1250]) ).
fof(f6908,plain,
connected(sK117),
inference(forward_subsumption_resolution,[],[f6907,f1934]) ).
fof(f6909,plain,
spl125_100,
inference(avatar_split_clause,[],[f6908,f6888]) ).
fof(f6910,plain,
( ~ relation(sK117)
| function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ transitive(sK116)
| transitive(sK117) ),
inference(resolution,[],[f1804,f1246]) ).
fof(f6911,plain,
( function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ transitive(sK116)
| transitive(sK117) ),
inference(forward_subsumption_resolution,[],[f6910,f1249]) ).
fof(f6912,plain,
( ~ relation(sK118)
| ~ relation(sK116)
| ~ transitive(sK116)
| transitive(sK117) ),
inference(forward_subsumption_resolution,[],[f6911,f1816]) ).
fof(f6913,plain,
( ~ relation(sK116)
| ~ transitive(sK116)
| transitive(sK117) ),
inference(forward_subsumption_resolution,[],[f6912,f1245]) ).
fof(f6914,plain,
( ~ transitive(sK116)
| transitive(sK117) ),
inference(forward_subsumption_resolution,[],[f6913,f1250]) ).
fof(f6916,definition,
( spl125_102
<=> transitive(sK116) ),
introduced(definition,[new_symbols(definition,[spl125_102])],[avatar_definition]) ).
fof(f6918,plain,
( ~ transitive(sK116)
| spl125_102 ),
inference(avatar_component_clause,[],[f6916]) ).
fof(f6919,plain,
( spl125_98
| ~ spl125_102 ),
inference(avatar_split_clause,[],[f6914,f6916,f6880]) ).
fof(f6920,plain,
( ~ relation(sK117)
| function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ reflexive(sK116)
| reflexive(sK117) ),
inference(resolution,[],[f1805,f1246]) ).
fof(f6921,plain,
( function(sK118)
| ~ relation(sK118)
| ~ relation(sK116)
| ~ reflexive(sK116)
| reflexive(sK117) ),
inference(forward_subsumption_resolution,[],[f6920,f1249]) ).
fof(f6922,plain,
( ~ relation(sK118)
| ~ relation(sK116)
| ~ reflexive(sK116)
| reflexive(sK117) ),
inference(forward_subsumption_resolution,[],[f6921,f1816]) ).
fof(f6923,plain,
( ~ relation(sK116)
| ~ reflexive(sK116)
| reflexive(sK117) ),
inference(forward_subsumption_resolution,[],[f6922,f1245]) ).
fof(f6924,plain,
( ~ reflexive(sK116)
| reflexive(sK117) ),
inference(forward_subsumption_resolution,[],[f6923,f1250]) ).
fof(f6925,plain,
( ~ reflexive(sK116)
| spl125_97 ),
inference(forward_subsumption_resolution,[],[f6924,f6878]) ).
fof(f7017,plain,
( ~ relation(sK116)
| ~ well_ordering(sK116)
| spl125_101 ),
inference(resolution,[],[f6901,f838]) ).
fof(f7018,plain,
( ~ well_ordering(sK116)
| spl125_101 ),
inference(forward_subsumption_resolution,[],[f7017,f1250]) ).
fof(f7019,plain,
( $false
| spl125_101 ),
inference(forward_subsumption_resolution,[],[f7018,f1247]) ).
fof(f7020,plain,
spl125_101,
inference(avatar_contradiction_clause,[],[f7019]) ).
fof(f7030,plain,
( ~ relation(sK116)
| ~ well_ordering(sK116)
| spl125_102 ),
inference(resolution,[],[f6918,f839]) ).
fof(f7031,plain,
( ~ well_ordering(sK116)
| spl125_102 ),
inference(forward_subsumption_resolution,[],[f7030,f1250]) ).
fof(f7032,plain,
( $false
| spl125_102 ),
inference(forward_subsumption_resolution,[],[f7031,f1247]) ).
fof(f7033,plain,
spl125_102,
inference(avatar_contradiction_clause,[],[f7032]) ).
fof(f7050,plain,
( ~ relation(sK116)
| ~ well_ordering(sK116)
| spl125_97 ),
inference(resolution,[],[f6925,f840]) ).
fof(f7051,plain,
( ~ well_ordering(sK116)
| spl125_97 ),
inference(forward_subsumption_resolution,[],[f7050,f1250]) ).
fof(f7052,plain,
( $false
| spl125_97 ),
inference(forward_subsumption_resolution,[],[f7051,f1247]) ).
fof(f7053,plain,
spl125_97,
inference(avatar_contradiction_clause,[],[f7052]) ).
cnf(s97,plain,
( ~ spl125_97
| ~ spl125_98
| ~ spl125_99
| ~ spl125_100 ),
inference(sat_conversion,[],[f6891]) ).
cnf(s98,plain,
( spl125_99
| ~ spl125_101 ),
inference(sat_conversion,[],[f6902]) ).
cnf(s99,plain,
spl125_100,
inference(sat_conversion,[],[f6909]) ).
cnf(s100,plain,
( spl125_98
| ~ spl125_102 ),
inference(sat_conversion,[],[f6919]) ).
cnf(s104,plain,
spl125_101,
inference(sat_conversion,[],[f7020]) ).
cnf(s105,plain,
spl125_102,
inference(sat_conversion,[],[f7033]) ).
cnf(s106,plain,
spl125_97,
inference(sat_conversion,[],[f7053]) ).
cnf(s107,plain,
spl125_98,
inference(rat,[],[s100,s105]) ).
cnf(s108,plain,
spl125_99,
inference(rat,[],[s98,s104]) ).
cnf(s109,plain,
$false,
inference(rat,[],[s97,s99,s108,s107,s106]) ).
fof(f7054,plain,
$false,
inference(avatar_sat_refutation,[],[s109]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU261+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.38 % Computer : n011.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Mon Sep 28 04:22:16 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.12/0.64 % (3014266)Will run a generic schedule for satisfiability detection.
% 1.12/0.64 % (3014276)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1783146856:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.12/0.64 % (3014272)% WARNING: option uhcvi not known.
% 1.12/0.64 % (3014271)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2884076740_2999 on theBenchmark for (2999ds/0Mi)
% 1.12/0.64 % (3014272)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2956940716:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.12/0.64 % (3014273)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3917114589:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.12/0.64 % (3014274)dis+10_1_sil=32000:sp=arity:random_seed=1115198901:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.12/0.64 % (3014275)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1165885589:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.12/0.64 % (3014277)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1203557706:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.12/0.64 % (3014276)Instruction limit reached!
% 1.12/0.64 % (3014276)------------------------------
% 1.12/0.64 % (3014276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.64 % (3014276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.64 % (3014276)CaDiCaL version: 2.1.3
% 1.12/0.64 % (3014276)Termination reason: Instruction limit
% 1.12/0.64 % (3014276)Termination phase: Saturation
% 1.12/0.64 % (3014276)Time elapsed: 0.039 s
% 1.12/0.64 % (3014276)Peak memory usage: 14 MB
% 1.12/0.64 % (3014276)Instructions burned: 131 (million)
% 1.12/0.64 % (3014285)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2904616681:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.12/0.64 % (3014274)Instruction limit reached!
% 1.12/0.64 % (3014274)------------------------------
% 1.12/0.64 % (3014274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.64 % (3014274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.64 % (3014274)CaDiCaL version: 2.1.3
% 1.12/0.64 % (3014274)Termination reason: Instruction limit
% 1.12/0.64 % (3014274)Termination phase: Saturation
% 1.12/0.64 % (3014274)Time elapsed: 0.066 s
% 1.12/0.64 % (3014274)Peak memory usage: 13 MB
% 1.12/0.64 % (3014274)Instructions burned: 103 (million)
% 1.12/0.64 % (3014275)Instruction limit reached!
% 1.12/0.64 % (3014275)------------------------------
% 1.12/0.64 % (3014275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.64 % (3014275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.64 % (3014275)CaDiCaL version: 2.1.3
% 1.12/0.64 % (3014275)Termination reason: Instruction limit
% 1.12/0.64 % (3014275)Termination phase: Saturation
% 1.12/0.64 % (3014275)Time elapsed: 0.069 s
% 1.12/0.64 % (3014275)Peak memory usage: 14 MB
% 1.12/0.64 % (3014275)Instructions burned: 116 (million)
% 1.12/0.64 % TRYING [1]
% 1.12/0.64 % TRYING [1]
% 1.12/0.64 % TRYING [2]
% 1.12/0.64 % TRYING [2]
% 1.12/0.64 % (3014287)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1161156759:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.12/0.64 % (3014288)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=3594343547:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.12/0.64 % TRYING [3]
% 1.12/0.64 % (3014277)Instruction limit reached!
% 1.12/0.64 % (3014277)------------------------------
% 1.12/0.64 % (3014277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.64 % (3014277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.64 % (3014277)CaDiCaL version: 2.1.3
% 1.12/0.64 % (3014277)Termination reason: Instruction limit
% 1.12/0.64 % (3014277)Termination phase: Saturation
% 1.12/0.64 % (3014277)Time elapsed: 0.099 s
% 1.12/0.64 % (3014277)Peak memory usage: 15 MB
% 1.12/0.64 % (3014277)Instructions burned: 160 (million)
% 1.12/0.64 % TRYING [3]
% 1.12/0.64 % (3014291)ott-21_1_sil=16000:fs=off:random_seed=3469657278:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.12/0.64 % (3014272) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3014266-3014272"...
% 1.12/0.64 % (3014272)...printing done.
% 1.12/0.64 % (3014272)Refutation found. Thanks to Tanya!
% 1.12/0.64 % SZS status Theorem for theBenchmark
% 1.12/0.64 % SZS output start Proof for theBenchmark
% See solution above
% 1.12/0.64 % (3014272)------------------------------
% 1.12/0.64 % (3014272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.64 % (3014272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.64 % (3014272)CaDiCaL version: 2.1.3
% 1.12/0.64 % (3014272)Termination reason: Refutation
% 1.12/0.64 % (3014272)Time elapsed: 0.157 s
% 1.12/0.64 % (3014272)Peak memory usage: 16 MB
% 1.12/0.64 % (3014272)Instructions burned: 238 (million)
% 1.12/0.64 % (3014266)Success in time 0.216 s
% 1.12/0.64 % Vampire exiting
%------------------------------------------------------------------------------