%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU244+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:34 PM UTC 2026
% Result : Theorem 4.97s 1.16s
% Output : Refutation 4.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 21
% Syntax : Number of formulae : 186 ( 17 unt; 13 def)
% Number of atoms : 572 ( 2 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 683 ( 297 ~; 300 |; 48 &)
% ( 28 <=>; 9 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 13 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-1 aty)
% Number of variables : 60 ( 0 sgn 57 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0] :
( relation(X0)
=> ( antisymmetric(X0)
<=> is_antisymmetric_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_relat_2) ).
fof(f22,axiom,
! [X0] :
( relation(X0)
=> ( connected(X0)
<=> is_connected_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d14_relat_2) ).
fof(f23,axiom,
! [X0] :
( relation(X0)
=> ( transitive(X0)
<=> is_transitive_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_relat_2) ).
fof(f50,axiom,
! [X0] :
( relation(X0)
=> ( well_ordering(X0)
<=> ( reflexive(X0)
& transitive(X0)
& antisymmetric(X0)
& connected(X0)
& well_founded_relation(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_wellord1) ).
fof(f56,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( well_orders(X0,X1)
<=> ( is_reflexive_in(X0,X1)
& is_transitive_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_connected_in(X0,X1)
& is_well_founded_in(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_wellord1) ).
fof(f68,axiom,
! [X0] :
( relation(X0)
=> ( reflexive(X0)
<=> is_reflexive_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_relat_2) ).
fof(f266,axiom,
! [X0] :
( relation(X0)
=> ( well_founded_relation(X0)
<=> is_well_founded_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_wellord1) ).
fof(f290,conjecture,
! [X0] :
( relation(X0)
=> ( well_orders(X0,relation_field(X0))
<=> well_ordering(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_wellord1) ).
fof(f291,negated_conjecture,
~ ! [X0] :
( relation(X0)
=> ( well_orders(X0,relation_field(X0))
<=> well_ordering(X0) ) ),
inference(negated_conjecture,[status(cth)],[f290]) ).
fof(f330,plain,
! [X0] :
( ( antisymmetric(X0)
<=> is_antisymmetric_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f335,plain,
! [X0] :
( ( connected(X0)
<=> is_connected_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f336,plain,
! [X0] :
( ( transitive(X0)
<=> is_transitive_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f354,plain,
! [X0] :
( ( well_ordering(X0)
<=> ( reflexive(X0)
& transitive(X0)
& antisymmetric(X0)
& connected(X0)
& well_founded_relation(X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f359,plain,
! [X0] :
( ! [X1] :
( well_orders(X0,X1)
<=> ( is_reflexive_in(X0,X1)
& is_transitive_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_connected_in(X0,X1)
& is_well_founded_in(X0,X1) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f373,plain,
! [X0] :
( ( reflexive(X0)
<=> is_reflexive_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f553,plain,
! [X0] :
( ( well_founded_relation(X0)
<=> is_well_founded_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f266]) ).
fof(f578,plain,
? [X0] :
( ( well_orders(X0,relation_field(X0))
<~> well_ordering(X0) )
& relation(X0) ),
inference(ennf_transformation,[],[f291]) ).
fof(f608,plain,
! [X0] :
( ( ( antisymmetric(X0)
| ~ is_antisymmetric_in(X0,relation_field(X0)) )
& ( is_antisymmetric_in(X0,relation_field(X0))
| ~ antisymmetric(X0) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f330]) ).
fof(f619,plain,
! [X0] :
( ( ( connected(X0)
| ~ is_connected_in(X0,relation_field(X0)) )
& ( is_connected_in(X0,relation_field(X0))
| ~ connected(X0) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f335]) ).
fof(f620,plain,
! [X0] :
( ( ( transitive(X0)
| ~ is_transitive_in(X0,relation_field(X0)) )
& ( is_transitive_in(X0,relation_field(X0))
| ~ transitive(X0) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f336]) ).
fof(f692,plain,
! [X0] :
( ( ( well_ordering(X0)
| ~ reflexive(X0)
| ~ transitive(X0)
| ~ antisymmetric(X0)
| ~ connected(X0)
| ~ well_founded_relation(X0) )
& ( ( reflexive(X0)
& transitive(X0)
& antisymmetric(X0)
& connected(X0)
& well_founded_relation(X0) )
| ~ well_ordering(X0) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f354]) ).
fof(f693,plain,
! [X0] :
( ( ( well_ordering(X0)
| ~ reflexive(X0)
| ~ transitive(X0)
| ~ antisymmetric(X0)
| ~ connected(X0)
| ~ well_founded_relation(X0) )
& ( ( reflexive(X0)
& transitive(X0)
& antisymmetric(X0)
& connected(X0)
& well_founded_relation(X0) )
| ~ well_ordering(X0) ) )
| ~ relation(X0) ),
inference(flattening,[],[f692]) ).
fof(f704,plain,
! [X0] :
( ! [X1] :
( ( well_orders(X0,X1)
| ~ is_reflexive_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ is_well_founded_in(X0,X1) )
& ( ( is_reflexive_in(X0,X1)
& is_transitive_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_connected_in(X0,X1)
& is_well_founded_in(X0,X1) )
| ~ well_orders(X0,X1) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f359]) ).
fof(f705,plain,
! [X0] :
( ! [X1] :
( ( well_orders(X0,X1)
| ~ is_reflexive_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ is_well_founded_in(X0,X1) )
& ( ( is_reflexive_in(X0,X1)
& is_transitive_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_connected_in(X0,X1)
& is_well_founded_in(X0,X1) )
| ~ well_orders(X0,X1) ) )
| ~ relation(X0) ),
inference(flattening,[],[f704]) ).
fof(f727,plain,
! [X0] :
( ( ( reflexive(X0)
| ~ is_reflexive_in(X0,relation_field(X0)) )
& ( is_reflexive_in(X0,relation_field(X0))
| ~ reflexive(X0) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f373]) ).
fof(f809,plain,
! [X0] :
( ( ( well_founded_relation(X0)
| ~ is_well_founded_in(X0,relation_field(X0)) )
& ( is_well_founded_in(X0,relation_field(X0))
| ~ well_founded_relation(X0) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f553]) ).
fof(f824,plain,
? [X0] :
( ( ~ well_ordering(X0)
| ~ well_orders(X0,relation_field(X0)) )
& ( well_ordering(X0)
| well_orders(X0,relation_field(X0)) )
& relation(X0) ),
inference(nnf_transformation,[],[f578]) ).
fof(f825,plain,
? [X0] :
( ( ~ well_ordering(X0)
| ~ well_orders(X0,relation_field(X0)) )
& ( well_ordering(X0)
| well_orders(X0,relation_field(X0)) )
& relation(X0) ),
inference(flattening,[],[f824]) ).
fof(f826,plain,
( ( ~ well_ordering(sK118)
| ~ well_orders(sK118,relation_field(sK118)) )
& ( well_ordering(sK118)
| well_orders(sK118,relation_field(sK118)) )
& relation(sK118) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118]),skolemize(X0,sK118)],[f825]) ).
fof(f874,plain,
! [X0] :
( ~ antisymmetric(X0)
| is_antisymmetric_in(X0,relation_field(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f608]) ).
fof(f875,plain,
! [X0] :
( ~ is_antisymmetric_in(X0,relation_field(X0))
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f608]) ).
fof(f894,plain,
! [X0] :
( ~ connected(X0)
| is_connected_in(X0,relation_field(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f619]) ).
fof(f895,plain,
! [X0] :
( ~ is_connected_in(X0,relation_field(X0))
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f619]) ).
fof(f896,plain,
! [X0] :
( ~ transitive(X0)
| is_transitive_in(X0,relation_field(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f620]) ).
fof(f897,plain,
! [X0] :
( ~ is_transitive_in(X0,relation_field(X0))
| transitive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f620]) ).
fof(f1014,plain,
! [X0] :
( ~ well_ordering(X0)
| well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1015,plain,
! [X0] :
( ~ well_ordering(X0)
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1016,plain,
! [X0] :
( ~ well_ordering(X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1017,plain,
! [X0] :
( ~ well_ordering(X0)
| transitive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1018,plain,
! [X0] :
( ~ well_ordering(X0)
| reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1019,plain,
! [X0] :
( ~ reflexive(X0)
| well_ordering(X0)
| ~ transitive(X0)
| ~ antisymmetric(X0)
| ~ connected(X0)
| ~ well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1038,plain,
! [X0,X1] :
( ~ well_orders(X0,X1)
| is_well_founded_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1039,plain,
! [X0,X1] :
( ~ well_orders(X0,X1)
| is_connected_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1040,plain,
! [X0,X1] :
( ~ well_orders(X0,X1)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1041,plain,
! [X0,X1] :
( ~ well_orders(X0,X1)
| is_transitive_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1042,plain,
! [X0,X1] :
( ~ well_orders(X0,X1)
| is_reflexive_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1043,plain,
! [X0,X1] :
( ~ is_well_founded_in(X0,X1)
| ~ is_reflexive_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ~ is_connected_in(X0,X1)
| well_orders(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1084,plain,
! [X0] :
( ~ reflexive(X0)
| is_reflexive_in(X0,relation_field(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f727]) ).
fof(f1085,plain,
! [X0] :
( ~ is_reflexive_in(X0,relation_field(X0))
| reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f727]) ).
fof(f1391,plain,
! [X0] :
( ~ well_founded_relation(X0)
| is_well_founded_in(X0,relation_field(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f809]) ).
fof(f1392,plain,
! [X0] :
( ~ is_well_founded_in(X0,relation_field(X0))
| well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f809]) ).
fof(f1432,plain,
relation(sK118),
inference(cnf_transformation,[],[f826]) ).
fof(f1433,plain,
( well_ordering(sK118)
| well_orders(sK118,relation_field(sK118)) ),
inference(cnf_transformation,[],[f826]) ).
fof(f1434,plain,
( ~ well_ordering(sK118)
| ~ well_orders(sK118,relation_field(sK118)) ),
inference(cnf_transformation,[],[f826]) ).
fof(f1728,definition,
sF121 = relation_field(sK118),
introduced(definition,[new_symbols(definition,[sF121])],[function_definition]) ).
fof(f1729,plain,
relation_field(sK118) = sF121,
inference(reorient_equations,[],[f1728]) ).
fof(f1730,plain,
( ~ well_ordering(sK118)
| ~ well_orders(sK118,sF121) ),
inference(definition_folding,[],[f1434,f1729]) ).
fof(f1731,plain,
( well_ordering(sK118)
| well_orders(sK118,sF121) ),
inference(definition_folding,[],[f1433,f1729]) ).
fof(f1735,definition,
( spl122_1
<=> well_orders(sK118,sF121) ),
introduced(definition,[new_symbols(definition,[spl122_1])],[avatar_definition]) ).
fof(f1736,plain,
( ~ well_orders(sK118,sF121)
| spl122_1 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1737,plain,
( well_orders(sK118,sF121)
| ~ spl122_1 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1739,definition,
( spl122_2
<=> well_ordering(sK118) ),
introduced(definition,[new_symbols(definition,[spl122_2])],[avatar_definition]) ).
fof(f1740,plain,
( ~ well_ordering(sK118)
| spl122_2 ),
inference(avatar_component_clause,[],[f1739]) ).
fof(f1741,plain,
( well_ordering(sK118)
| ~ spl122_2 ),
inference(avatar_component_clause,[],[f1739]) ).
fof(f1742,plain,
( spl122_1
| spl122_2 ),
inference(avatar_split_clause,[],[f1731,f1739,f1735]) ).
fof(f1743,plain,
( ~ spl122_1
| ~ spl122_2 ),
inference(avatar_split_clause,[],[f1730,f1739,f1735]) ).
fof(f1961,plain,
( well_founded_relation(sK118)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f1014,f1741]) ).
fof(f1962,plain,
( well_founded_relation(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f1961,f1432]) ).
fof(f1963,plain,
( connected(sK118)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f1015,f1741]) ).
fof(f1964,plain,
( connected(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f1963,f1432]) ).
fof(f1965,plain,
( antisymmetric(sK118)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f1016,f1741]) ).
fof(f1966,plain,
( antisymmetric(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f1965,f1432]) ).
fof(f1967,plain,
( transitive(sK118)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f1017,f1741]) ).
fof(f1968,plain,
( transitive(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f1967,f1432]) ).
fof(f1969,plain,
( reflexive(sK118)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f1018,f1741]) ).
fof(f1970,plain,
( reflexive(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f1969,f1432]) ).
fof(f2692,plain,
( is_well_founded_in(sK118,relation_field(sK118))
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f1391,f1962]) ).
fof(f2693,plain,
( is_well_founded_in(sK118,relation_field(sK118))
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f2692,f1432]) ).
fof(f2694,plain,
( is_well_founded_in(sK118,sF121)
| ~ spl122_2 ),
inference(forward_demodulation,[],[f2693,f1729]) ).
fof(f2695,plain,
( ~ is_well_founded_in(sK118,sF121)
| well_founded_relation(sK118)
| ~ relation(sK118) ),
inference(superposition,[],[f1392,f1729]) ).
fof(f2898,plain,
( is_antisymmetric_in(sK118,relation_field(sK118))
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f874,f1966]) ).
fof(f2899,plain,
( is_antisymmetric_in(sK118,relation_field(sK118))
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f2898,f1432]) ).
fof(f2900,plain,
( is_antisymmetric_in(sK118,sF121)
| ~ spl122_2 ),
inference(forward_demodulation,[],[f2899,f1729]) ).
fof(f2901,plain,
( ~ is_antisymmetric_in(sK118,sF121)
| antisymmetric(sK118)
| ~ relation(sK118) ),
inference(superposition,[],[f875,f1729]) ).
fof(f2903,plain,
( is_connected_in(sK118,relation_field(sK118))
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f894,f1964]) ).
fof(f2904,plain,
( is_connected_in(sK118,relation_field(sK118))
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f2903,f1432]) ).
fof(f2905,plain,
( is_connected_in(sK118,sF121)
| ~ spl122_2 ),
inference(forward_demodulation,[],[f2904,f1729]) ).
fof(f2906,plain,
( ~ is_connected_in(sK118,sF121)
| connected(sK118)
| ~ relation(sK118) ),
inference(superposition,[],[f895,f1729]) ).
fof(f2909,plain,
( is_transitive_in(sK118,relation_field(sK118))
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f896,f1968]) ).
fof(f2910,plain,
( is_transitive_in(sK118,relation_field(sK118))
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f2909,f1432]) ).
fof(f2911,plain,
( is_transitive_in(sK118,sF121)
| ~ spl122_2 ),
inference(forward_demodulation,[],[f2910,f1729]) ).
fof(f2912,plain,
( ~ is_transitive_in(sK118,sF121)
| transitive(sK118)
| ~ relation(sK118) ),
inference(superposition,[],[f897,f1729]) ).
fof(f2997,plain,
( is_reflexive_in(sK118,relation_field(sK118))
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f1084,f1970]) ).
fof(f2998,plain,
( is_reflexive_in(sK118,relation_field(sK118))
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f2997,f1432]) ).
fof(f2999,plain,
( is_reflexive_in(sK118,sF121)
| ~ spl122_2 ),
inference(forward_demodulation,[],[f2998,f1729]) ).
fof(f3000,plain,
( ~ is_reflexive_in(sK118,sF121)
| reflexive(sK118)
| ~ relation(sK118) ),
inference(superposition,[],[f1085,f1729]) ).
fof(f16386,plain,
( ~ is_reflexive_in(sK118,sF121)
| ~ is_transitive_in(sK118,sF121)
| ~ is_antisymmetric_in(sK118,sF121)
| ~ is_connected_in(sK118,sF121)
| well_orders(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(resolution,[],[f1043,f2694]) ).
fof(f16389,plain,
( ~ is_transitive_in(sK118,sF121)
| ~ is_antisymmetric_in(sK118,sF121)
| ~ is_connected_in(sK118,sF121)
| well_orders(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f16386,f2999]) ).
fof(f16391,plain,
( ~ is_antisymmetric_in(sK118,sF121)
| ~ is_connected_in(sK118,sF121)
| well_orders(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f16389,f2911]) ).
fof(f16393,plain,
( ~ is_connected_in(sK118,sF121)
| well_orders(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f16391,f2900]) ).
fof(f16395,plain,
( well_orders(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f16393,f2905]) ).
fof(f16397,plain,
( ~ relation(sK118)
| spl122_1
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f16395,f1736]) ).
fof(f16399,plain,
( $false
| spl122_1
| ~ spl122_2 ),
inference(forward_subsumption_resolution,[],[f16397,f1432]) ).
fof(f16400,plain,
( spl122_1
| ~ spl122_2 ),
inference(avatar_contradiction_clause,[],[f16399]) ).
fof(f16414,plain,
( ~ is_well_founded_in(sK118,sF121)
| well_founded_relation(sK118) ),
inference(forward_subsumption_resolution,[],[f2695,f1432]) ).
fof(f16415,plain,
( ~ is_antisymmetric_in(sK118,sF121)
| antisymmetric(sK118) ),
inference(forward_subsumption_resolution,[],[f2901,f1432]) ).
fof(f16416,plain,
( ~ is_connected_in(sK118,sF121)
| connected(sK118) ),
inference(forward_subsumption_resolution,[],[f2906,f1432]) ).
fof(f16417,plain,
( ~ is_transitive_in(sK118,sF121)
| transitive(sK118) ),
inference(forward_subsumption_resolution,[],[f2912,f1432]) ).
fof(f16418,plain,
( ~ is_reflexive_in(sK118,sF121)
| reflexive(sK118) ),
inference(forward_subsumption_resolution,[],[f3000,f1432]) ).
fof(f16431,definition,
( spl122_271
<=> well_founded_relation(sK118) ),
introduced(definition,[new_symbols(definition,[spl122_271])],[avatar_definition]) ).
fof(f16433,plain,
( well_founded_relation(sK118)
| ~ spl122_271 ),
inference(avatar_component_clause,[],[f16431]) ).
fof(f16435,definition,
( spl122_272
<=> is_well_founded_in(sK118,sF121) ),
introduced(definition,[new_symbols(definition,[spl122_272])],[avatar_definition]) ).
fof(f16437,plain,
( ~ is_well_founded_in(sK118,sF121)
| spl122_272 ),
inference(avatar_component_clause,[],[f16435]) ).
fof(f16438,plain,
( spl122_271
| ~ spl122_272 ),
inference(avatar_split_clause,[],[f16414,f16435,f16431]) ).
fof(f16440,definition,
( spl122_273
<=> antisymmetric(sK118) ),
introduced(definition,[new_symbols(definition,[spl122_273])],[avatar_definition]) ).
fof(f16442,plain,
( antisymmetric(sK118)
| ~ spl122_273 ),
inference(avatar_component_clause,[],[f16440]) ).
fof(f16444,definition,
( spl122_274
<=> is_antisymmetric_in(sK118,sF121) ),
introduced(definition,[new_symbols(definition,[spl122_274])],[avatar_definition]) ).
fof(f16446,plain,
( ~ is_antisymmetric_in(sK118,sF121)
| spl122_274 ),
inference(avatar_component_clause,[],[f16444]) ).
fof(f16447,plain,
( spl122_273
| ~ spl122_274 ),
inference(avatar_split_clause,[],[f16415,f16444,f16440]) ).
fof(f16449,definition,
( spl122_275
<=> connected(sK118) ),
introduced(definition,[new_symbols(definition,[spl122_275])],[avatar_definition]) ).
fof(f16451,plain,
( connected(sK118)
| ~ spl122_275 ),
inference(avatar_component_clause,[],[f16449]) ).
fof(f16453,definition,
( spl122_276
<=> is_connected_in(sK118,sF121) ),
introduced(definition,[new_symbols(definition,[spl122_276])],[avatar_definition]) ).
fof(f16456,plain,
( spl122_275
| ~ spl122_276 ),
inference(avatar_split_clause,[],[f16416,f16453,f16449]) ).
fof(f16458,definition,
( spl122_277
<=> transitive(sK118) ),
introduced(definition,[new_symbols(definition,[spl122_277])],[avatar_definition]) ).
fof(f16460,plain,
( transitive(sK118)
| ~ spl122_277 ),
inference(avatar_component_clause,[],[f16458]) ).
fof(f16462,definition,
( spl122_278
<=> is_transitive_in(sK118,sF121) ),
introduced(definition,[new_symbols(definition,[spl122_278])],[avatar_definition]) ).
fof(f16465,plain,
( spl122_277
| ~ spl122_278 ),
inference(avatar_split_clause,[],[f16417,f16462,f16458]) ).
fof(f16467,definition,
( spl122_279
<=> reflexive(sK118) ),
introduced(definition,[new_symbols(definition,[spl122_279])],[avatar_definition]) ).
fof(f16469,plain,
( reflexive(sK118)
| ~ spl122_279 ),
inference(avatar_component_clause,[],[f16467]) ).
fof(f16471,definition,
( spl122_280
<=> is_reflexive_in(sK118,sF121) ),
introduced(definition,[new_symbols(definition,[spl122_280])],[avatar_definition]) ).
fof(f16473,plain,
( ~ is_reflexive_in(sK118,sF121)
| spl122_280 ),
inference(avatar_component_clause,[],[f16471]) ).
fof(f16474,plain,
( spl122_279
| ~ spl122_280 ),
inference(avatar_split_clause,[],[f16418,f16471,f16467]) ).
fof(f16527,plain,
( is_reflexive_in(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_1 ),
inference(resolution,[],[f1737,f1042]) ).
fof(f16528,plain,
( is_transitive_in(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_1 ),
inference(resolution,[],[f1737,f1041]) ).
fof(f16529,plain,
( is_antisymmetric_in(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_1 ),
inference(resolution,[],[f1737,f1040]) ).
fof(f16530,plain,
( is_connected_in(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_1 ),
inference(resolution,[],[f1737,f1039]) ).
fof(f16531,plain,
( is_well_founded_in(sK118,sF121)
| ~ relation(sK118)
| ~ spl122_1 ),
inference(resolution,[],[f1737,f1038]) ).
fof(f16532,plain,
( ~ relation(sK118)
| ~ spl122_1
| spl122_272 ),
inference(forward_subsumption_resolution,[],[f16531,f16437]) ).
fof(f16533,plain,
( is_connected_in(sK118,sF121)
| ~ spl122_1 ),
inference(forward_subsumption_resolution,[],[f16530,f1432]) ).
fof(f16534,plain,
( ~ relation(sK118)
| ~ spl122_1
| spl122_274 ),
inference(forward_subsumption_resolution,[],[f16529,f16446]) ).
fof(f16535,plain,
( is_transitive_in(sK118,sF121)
| ~ spl122_1 ),
inference(forward_subsumption_resolution,[],[f16528,f1432]) ).
fof(f16536,plain,
( ~ relation(sK118)
| ~ spl122_1
| spl122_280 ),
inference(forward_subsumption_resolution,[],[f16527,f16473]) ).
fof(f16537,plain,
( $false
| ~ spl122_1
| spl122_272 ),
inference(forward_subsumption_resolution,[],[f16532,f1432]) ).
fof(f16538,plain,
( ~ spl122_1
| spl122_272 ),
inference(avatar_contradiction_clause,[],[f16537]) ).
fof(f16539,plain,
( spl122_276
| ~ spl122_1 ),
inference(avatar_split_clause,[],[f16533,f1735,f16453]) ).
fof(f16540,plain,
( $false
| ~ spl122_1
| spl122_274 ),
inference(forward_subsumption_resolution,[],[f16534,f1432]) ).
fof(f16541,plain,
( ~ spl122_1
| spl122_274 ),
inference(avatar_contradiction_clause,[],[f16540]) ).
fof(f16542,plain,
( spl122_278
| ~ spl122_1 ),
inference(avatar_split_clause,[],[f16535,f1735,f16462]) ).
fof(f16543,plain,
( $false
| ~ spl122_1
| spl122_280 ),
inference(forward_subsumption_resolution,[],[f16536,f1432]) ).
fof(f16544,plain,
( ~ spl122_1
| spl122_280 ),
inference(avatar_contradiction_clause,[],[f16543]) ).
fof(f16724,plain,
( well_ordering(sK118)
| ~ transitive(sK118)
| ~ antisymmetric(sK118)
| ~ connected(sK118)
| ~ well_founded_relation(sK118)
| ~ relation(sK118)
| ~ spl122_279 ),
inference(resolution,[],[f16469,f1019]) ).
fof(f16727,plain,
( ~ transitive(sK118)
| ~ antisymmetric(sK118)
| ~ connected(sK118)
| ~ well_founded_relation(sK118)
| ~ relation(sK118)
| spl122_2
| ~ spl122_279 ),
inference(forward_subsumption_resolution,[],[f16724,f1740]) ).
fof(f16729,plain,
( ~ antisymmetric(sK118)
| ~ connected(sK118)
| ~ well_founded_relation(sK118)
| ~ relation(sK118)
| spl122_2
| ~ spl122_277
| ~ spl122_279 ),
inference(forward_subsumption_resolution,[],[f16727,f16460]) ).
fof(f16730,plain,
( ~ connected(sK118)
| ~ well_founded_relation(sK118)
| ~ relation(sK118)
| spl122_2
| ~ spl122_273
| ~ spl122_277
| ~ spl122_279 ),
inference(forward_subsumption_resolution,[],[f16729,f16442]) ).
fof(f16731,plain,
( ~ well_founded_relation(sK118)
| ~ relation(sK118)
| spl122_2
| ~ spl122_273
| ~ spl122_275
| ~ spl122_277
| ~ spl122_279 ),
inference(forward_subsumption_resolution,[],[f16730,f16451]) ).
fof(f16732,plain,
( ~ relation(sK118)
| spl122_2
| ~ spl122_271
| ~ spl122_273
| ~ spl122_275
| ~ spl122_277
| ~ spl122_279 ),
inference(forward_subsumption_resolution,[],[f16731,f16433]) ).
fof(f16733,plain,
( $false
| spl122_2
| ~ spl122_271
| ~ spl122_273
| ~ spl122_275
| ~ spl122_277
| ~ spl122_279 ),
inference(forward_subsumption_resolution,[],[f16732,f1432]) ).
fof(f16734,plain,
( spl122_2
| ~ spl122_271
| ~ spl122_273
| ~ spl122_275
| ~ spl122_277
| ~ spl122_279 ),
inference(avatar_contradiction_clause,[],[f16733]) ).
cnf(s1,plain,
( spl122_1
| spl122_2 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s2,plain,
( ~ spl122_1
| ~ spl122_2 ),
inference(sat_conversion,[],[f1743]) ).
cnf(s215,plain,
( spl122_1
| ~ spl122_2 ),
inference(sat_conversion,[],[f16400]) ).
cnf(s217,plain,
( spl122_271
| ~ spl122_272 ),
inference(sat_conversion,[],[f16438]) ).
cnf(s218,plain,
( spl122_273
| ~ spl122_274 ),
inference(sat_conversion,[],[f16447]) ).
cnf(s219,plain,
( spl122_275
| ~ spl122_276 ),
inference(sat_conversion,[],[f16456]) ).
cnf(s220,plain,
( spl122_277
| ~ spl122_278 ),
inference(sat_conversion,[],[f16465]) ).
cnf(s221,plain,
( spl122_279
| ~ spl122_280 ),
inference(sat_conversion,[],[f16474]) ).
cnf(s233,plain,
( ~ spl122_1
| spl122_272 ),
inference(sat_conversion,[],[f16538]) ).
cnf(s234,plain,
( ~ spl122_1
| spl122_276 ),
inference(sat_conversion,[],[f16539]) ).
cnf(s235,plain,
( ~ spl122_1
| spl122_274 ),
inference(sat_conversion,[],[f16541]) ).
cnf(s236,plain,
( ~ spl122_1
| spl122_278 ),
inference(sat_conversion,[],[f16542]) ).
cnf(s237,plain,
( ~ spl122_1
| spl122_280 ),
inference(sat_conversion,[],[f16544]) ).
cnf(s238,plain,
( spl122_2
| ~ spl122_271
| ~ spl122_273
| ~ spl122_275
| ~ spl122_277
| ~ spl122_279 ),
inference(sat_conversion,[],[f16734]) ).
cnf(s255,plain,
spl122_1,
inference(rat,[],[s1,s215]) ).
cnf(s256,plain,
spl122_280,
inference(rat,[],[s237,s255]) ).
cnf(s257,plain,
spl122_278,
inference(rat,[],[s236,s255]) ).
cnf(s258,plain,
spl122_274,
inference(rat,[],[s235,s255]) ).
cnf(s259,plain,
spl122_276,
inference(rat,[],[s234,s255]) ).
cnf(s260,plain,
spl122_272,
inference(rat,[],[s233,s255]) ).
cnf(s261,plain,
~ spl122_2,
inference(rat,[],[s2,s255]) ).
cnf(s262,plain,
spl122_279,
inference(rat,[],[s221,s256]) ).
cnf(s263,plain,
spl122_277,
inference(rat,[],[s220,s257]) ).
cnf(s264,plain,
spl122_273,
inference(rat,[],[s218,s258]) ).
cnf(s265,plain,
spl122_275,
inference(rat,[],[s219,s259]) ).
cnf(s266,plain,
spl122_271,
inference(rat,[],[s217,s260]) ).
cnf(s267,plain,
$false,
inference(rat,[],[s238,s262,s263,s265,s264,s266,s261]) ).
fof(f16735,plain,
$false,
inference(avatar_sat_refutation,[],[s267]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU244+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n017.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 28 04:12:35 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.97/1.16 % (3193848)Will run a generic schedule for satisfiability detection.
% 4.97/1.16 % (3193857)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=874621020:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.97/1.16 % (3193854)% WARNING: option uhcvi not known.
% 4.97/1.16 % (3193854)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1310569406:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.97/1.16 % (3193853)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3535429979_2999 on theBenchmark for (2999ds/0Mi)
% 4.97/1.16 % (3193855)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=950478299:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.97/1.16 % (3193856)dis+10_1_sil=32000:sp=arity:random_seed=780059433:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.97/1.16 % (3193859)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3341478294:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.97/1.16 % (3193858)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3972023995:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.97/1.16 % (3193857)Instruction limit reached!
% 4.97/1.16 % (3193857)------------------------------
% 4.97/1.16 % (3193857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193857)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193857)Termination reason: Instruction limit
% 4.97/1.16 % (3193857)Termination phase: Saturation
% 4.97/1.16 % (3193857)Time elapsed: 0.040 s
% 4.97/1.16 % (3193857)Peak memory usage: 14 MB
% 4.97/1.16 % (3193857)Instructions burned: 118 (million)
% 4.97/1.16 % (3193867)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1490544685:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.97/1.16 % TRYING [1]
% 4.97/1.16 % (3193856)Instruction limit reached!
% 4.97/1.16 % (3193856)------------------------------
% 4.97/1.16 % (3193856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193856)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193856)Termination reason: Instruction limit
% 4.97/1.16 % (3193856)Termination phase: Saturation
% 4.97/1.16 % (3193856)Time elapsed: 0.070 s
% 4.97/1.16 % (3193856)Peak memory usage: 13 MB
% 4.97/1.16 % (3193856)Instructions burned: 106 (million)
% 4.97/1.16 % (3193858)Instruction limit reached!
% 4.97/1.16 % (3193858)------------------------------
% 4.97/1.16 % (3193858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193858)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193858)Termination reason: Instruction limit
% 4.97/1.16 % (3193858)Termination phase: Saturation
% 4.97/1.16 % (3193858)Time elapsed: 0.069 s
% 4.97/1.16 % (3193858)Peak memory usage: 14 MB
% 4.97/1.16 % (3193858)Instructions burned: 132 (million)
% 4.97/1.16 % TRYING [2]
% 4.97/1.16 % (3193869)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=372121077:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.97/1.16 % (3193870)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=2156826322:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.97/1.16 % TRYING [1]
% 4.97/1.16 % TRYING [2]
% 4.97/1.16 % (3193859)Instruction limit reached!
% 4.97/1.16 % (3193859)------------------------------
% 4.97/1.16 % (3193859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193859)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193859)Termination reason: Instruction limit
% 4.97/1.16 % (3193859)Termination phase: Saturation
% 4.97/1.16 % (3193859)Time elapsed: 0.100 s
% 4.97/1.16 % (3193859)Peak memory usage: 14 MB
% 4.97/1.16 % (3193859)Instructions burned: 160 (million)
% 4.97/1.16 % TRYING [3]
% 4.97/1.16 % TRYING [3]
% 4.97/1.16 % (3193873)ott-21_1_sil=16000:fs=off:random_seed=4081351167:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.97/1.16 % (3193869)Instruction limit reached!
% 4.97/1.16 % (3193869)------------------------------
% 4.97/1.16 % (3193869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193869)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193869)Termination reason: Instruction limit
% 4.97/1.16 % (3193869)Termination phase: Saturation
% 4.97/1.16 % (3193869)Time elapsed: 0.076 s
% 4.97/1.16 % (3193869)Peak memory usage: 13 MB
% 4.97/1.16 % (3193869)Instructions burned: 131 (million)
% 4.97/1.16 % (3193875)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1269809909:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 4.97/1.16 % TRYING [4]
% 4.97/1.16 % (3193867)Instruction limit reached!
% 4.97/1.16 % (3193867)------------------------------
% 4.97/1.16 % (3193867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193867)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193867)Termination reason: Instruction limit
% 4.97/1.16 % (3193867)Termination phase: Finite model building constraint generation
% 4.97/1.16 % (3193867)Time elapsed: 0.164 s
% 4.97/1.16 % (3193867)Peak memory usage: 35 MB
% 4.97/1.16 % (3193867)Instructions burned: 718 (million)
% 4.97/1.16 % (3193873)Instruction limit reached!
% 4.97/1.16 % (3193873)------------------------------
% 4.97/1.16 % (3193873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193873)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193873)Termination reason: Instruction limit
% 4.97/1.16 % (3193873)Termination phase: Saturation
% 4.97/1.16 % (3193873)Time elapsed: 0.100 s
% 4.97/1.16 % (3193873)Peak memory usage: 14 MB
% 4.97/1.16 % (3193873)Instructions burned: 182 (million)
% 4.97/1.16 % (3193877)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=604405263:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.97/1.16 % (3193878)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3527098138:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 4.97/1.16 % TRYING [1]
% 4.97/1.16 % TRYING [2]
% 4.97/1.16 % TRYING [4]
% 4.97/1.16 % TRYING [3]
% 4.97/1.16 % (3193877)Instruction limit reached!
% 4.97/1.16 % (3193877)------------------------------
% 4.97/1.16 % (3193877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193877)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193877)Termination reason: Instruction limit
% 4.97/1.16 % (3193877)Termination phase: Finite model building SAT solving
% 4.97/1.16 % (3193877)Time elapsed: 0.209 s
% 4.97/1.16 % (3193877)Peak memory usage: 39 MB
% 4.97/1.16 % (3193877)Instructions burned: 868 (million)
% 4.97/1.16 % (3193881)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2859090410:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 4.97/1.16 % (3193870)Instruction limit reached!
% 4.97/1.16 % (3193870)------------------------------
% 4.97/1.16 % (3193870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193870)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193870)Termination reason: Instruction limit
% 4.97/1.16 % (3193870)Termination phase: Saturation
% 4.97/1.16 % (3193870)Time elapsed: 0.413 s
% 4.97/1.16 % (3193870)Peak memory usage: 20 MB
% 4.97/1.16 % (3193870)Instructions burned: 686 (million)
% 4.97/1.16 % (3193875)Instruction limit reached!
% 4.97/1.16 % (3193875)------------------------------
% 4.97/1.16 % (3193875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.16 % (3193875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.16 % (3193875)CaDiCaL version: 2.1.3
% 4.97/1.16 % (3193875)Termination reason: Instruction limit
% 4.97/1.16 % (3193875)Termination phase: Saturation
% 4.97/1.16 % (3193875)Time elapsed: 0.336 s
% 4.97/1.16 % (3193875)Peak memory usage: 15 MB
% 4.97/1.16 % (3193875)Instructions burned: 478 (million)
% 4.97/1.16 % (3193883)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4289244439:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 4.97/1.16 % (3193884)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3574655425:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 4.97/1.16 % (3193878) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3193848-3193878"...
% 4.97/1.16 % (3193878)...printing done.
% 4.97/1.16 % (3193878)Refutation found. Thanks to Tanya!
% 4.97/1.16 % SZS status Theorem for theBenchmark
% 4.97/1.16 % SZS output start Proof for theBenchmark
% See solution above
% 4.97/1.17 % (3193878)------------------------------
% 4.97/1.17 % (3193878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.97/1.17 % (3193878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.17 % (3193878)CaDiCaL version: 2.1.3
% 4.97/1.17 % (3193878)Termination reason: Refutation
% 4.97/1.17 % (3193878)Time elapsed: 0.440 s
% 4.97/1.17 % (3193878)Peak memory usage: 22 MB
% 4.97/1.17 % (3193878)Instructions burned: 694 (million)
% 4.97/1.17 % (3193848)Success in time 0.735 s
% 4.97/1.17 % Vampire exiting
%------------------------------------------------------------------------------