%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MGT005+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:02:27 PM UTC 2026
% Result : Theorem 0.09s 0.45s
% Output : Refutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 15
% Syntax : Number of formulae : 126 ( 42 unt; 10 def)
% Number of atoms : 576 ( 31 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 750 ( 300 ~; 301 |; 129 &)
% ( 10 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 7 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 11 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 13 con; 0-0 aty)
% Number of variables : 230 ( 0 sgn 204 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0,X1,X2,X3] :
( ( organization(X0,X2)
& organization(X0,X3)
& greater(X1,X2)
& greater(X3,X1) )
=> organization(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp13) ).
fof(f7,axiom,
! [X0,X1,X2] :
( reorganization(X0,X1,X2)
=> greater(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp7) ).
fof(f10,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( organization(X0,X6)
& organization(X1,X6)
& organization(X1,X8)
& class(X0,X3,X6)
& class(X1,X3,X6)
& reorganization(X0,X6,X7)
& reorganization(X1,X6,X8)
& reorganization_type(X0,X2,X6)
& reorganization_type(X1,X2,X6)
& complexity(X0,X4,X6)
& complexity(X1,X5,X6)
& greater(X5,X4) )
=> greater(X8,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a10_FOL) ).
fof(f11,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( organization(X0,X9)
& organization(X1,X9)
& organization(X0,X10)
& organization(X1,X10)
& class(X0,X3,X9)
& class(X1,X3,X9)
& survival_chance(X0,X4,X9)
& survival_chance(X1,X4,X9)
& reorganization(X0,X9,X10)
& reorganization(X1,X9,X11)
& reorganization_type(X0,X2,X9)
& reorganization_type(X1,X2,X9)
& survival_chance(X0,X5,X10)
& survival_chance(X1,X6,X10)
& complexity(X0,X7,X9)
& complexity(X1,X8,X9)
& greater(X8,X7) )
=> ( greater(X5,X6)
| X5 = X6 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a11_FOL) ).
fof(f13,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ( organization(X0,X10)
& organization(X1,X10)
& organization(X0,X12)
& organization(X1,X12)
& class(X0,X3,X10)
& class(X1,X3,X10)
& survival_chance(X0,X4,X10)
& survival_chance(X1,X4,X10)
& reorganization(X0,X10,X11)
& reorganization(X1,X10,X12)
& reorganization_type(X0,X2,X10)
& reorganization_type(X1,X2,X10)
& reorganization_free(X0,X11,X12)
& survival_chance(X0,X5,X9)
& survival_chance(X1,X6,X9)
& complexity(X0,X7,X10)
& complexity(X1,X8,X10)
& greater(X8,X7)
& ( X9 = X12
=> greater(X5,X6) ) )
=> ( X9 = X11
=> ( greater(X5,X6)
| X5 = X6 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL) ).
fof(f14,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ( organization(X0,X10)
& organization(X1,X10)
& organization(X0,X12)
& organization(X1,X12)
& class(X0,X3,X10)
& class(X1,X3,X10)
& survival_chance(X0,X4,X10)
& survival_chance(X1,X4,X10)
& reorganization(X0,X10,X11)
& reorganization(X1,X10,X12)
& reorganization_type(X0,X2,X10)
& reorganization_type(X1,X2,X10)
& reorganization_free(X0,X11,X12)
& survival_chance(X0,X5,X9)
& survival_chance(X1,X6,X9)
& complexity(X0,X7,X10)
& complexity(X1,X8,X10)
& greater(X8,X7)
& ( X9 = X12
=> greater(X5,X6) ) )
=> ( X9 = X11
=> ( greater(X5,X6)
| X5 = X6 ) ) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f22,plain,
! [X0,X1,X2,X3] :
( organization(X0,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X3)
| ~ greater(X1,X2)
| ~ greater(X3,X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( organization(X0,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X3)
| ~ greater(X1,X2)
| ~ greater(X3,X1) ),
inference(flattening,[],[f22]) ).
fof(f24,plain,
! [X0,X1,X2] :
( greater(X2,X1)
| ~ reorganization(X0,X1,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f29,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( greater(X8,X7)
| ~ organization(X0,X6)
| ~ organization(X1,X6)
| ~ organization(X1,X8)
| ~ class(X0,X3,X6)
| ~ class(X1,X3,X6)
| ~ reorganization(X0,X6,X7)
| ~ reorganization(X1,X6,X8)
| ~ reorganization_type(X0,X2,X6)
| ~ reorganization_type(X1,X2,X6)
| ~ complexity(X0,X4,X6)
| ~ complexity(X1,X5,X6)
| ~ greater(X5,X4) ),
inference(ennf_transformation,[],[f10]) ).
fof(f30,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( greater(X8,X7)
| ~ organization(X0,X6)
| ~ organization(X1,X6)
| ~ organization(X1,X8)
| ~ class(X0,X3,X6)
| ~ class(X1,X3,X6)
| ~ reorganization(X0,X6,X7)
| ~ reorganization(X1,X6,X8)
| ~ reorganization_type(X0,X2,X6)
| ~ reorganization_type(X1,X2,X6)
| ~ complexity(X0,X4,X6)
| ~ complexity(X1,X5,X6)
| ~ greater(X5,X4) ),
inference(flattening,[],[f29]) ).
fof(f31,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( greater(X5,X6)
| X5 = X6
| ~ organization(X0,X9)
| ~ organization(X1,X9)
| ~ organization(X0,X10)
| ~ organization(X1,X10)
| ~ class(X0,X3,X9)
| ~ class(X1,X3,X9)
| ~ survival_chance(X0,X4,X9)
| ~ survival_chance(X1,X4,X9)
| ~ reorganization(X0,X9,X10)
| ~ reorganization(X1,X9,X11)
| ~ reorganization_type(X0,X2,X9)
| ~ reorganization_type(X1,X2,X9)
| ~ survival_chance(X0,X5,X10)
| ~ survival_chance(X1,X6,X10)
| ~ complexity(X0,X7,X9)
| ~ complexity(X1,X8,X9)
| ~ greater(X8,X7) ),
inference(ennf_transformation,[],[f11]) ).
fof(f32,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( greater(X5,X6)
| X5 = X6
| ~ organization(X0,X9)
| ~ organization(X1,X9)
| ~ organization(X0,X10)
| ~ organization(X1,X10)
| ~ class(X0,X3,X9)
| ~ class(X1,X3,X9)
| ~ survival_chance(X0,X4,X9)
| ~ survival_chance(X1,X4,X9)
| ~ reorganization(X0,X9,X10)
| ~ reorganization(X1,X9,X11)
| ~ reorganization_type(X0,X2,X9)
| ~ reorganization_type(X1,X2,X9)
| ~ survival_chance(X0,X5,X10)
| ~ survival_chance(X1,X6,X10)
| ~ complexity(X0,X7,X9)
| ~ complexity(X1,X8,X9)
| ~ greater(X8,X7) ),
inference(flattening,[],[f31]) ).
fof(f35,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ greater(X5,X6)
& X5 != X6
& X9 = X11
& organization(X0,X10)
& organization(X1,X10)
& organization(X0,X12)
& organization(X1,X12)
& class(X0,X3,X10)
& class(X1,X3,X10)
& survival_chance(X0,X4,X10)
& survival_chance(X1,X4,X10)
& reorganization(X0,X10,X11)
& reorganization(X1,X10,X12)
& reorganization_type(X0,X2,X10)
& reorganization_type(X1,X2,X10)
& reorganization_free(X0,X11,X12)
& survival_chance(X0,X5,X9)
& survival_chance(X1,X6,X9)
& complexity(X0,X7,X10)
& complexity(X1,X8,X10)
& greater(X8,X7)
& ( greater(X5,X6)
| X9 != X12 ) ),
inference(ennf_transformation,[],[f14]) ).
fof(f36,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ greater(X5,X6)
& X5 != X6
& X9 = X11
& organization(X0,X10)
& organization(X1,X10)
& organization(X0,X12)
& organization(X1,X12)
& class(X0,X3,X10)
& class(X1,X3,X10)
& survival_chance(X0,X4,X10)
& survival_chance(X1,X4,X10)
& reorganization(X0,X10,X11)
& reorganization(X1,X10,X12)
& reorganization_type(X0,X2,X10)
& reorganization_type(X1,X2,X10)
& reorganization_free(X0,X11,X12)
& survival_chance(X0,X5,X9)
& survival_chance(X1,X6,X9)
& complexity(X0,X7,X10)
& complexity(X1,X8,X10)
& greater(X8,X7)
& ( greater(X5,X6)
| X9 != X12 ) ),
inference(flattening,[],[f35]) ).
fof(f39,plain,
( ~ greater(sK9,sK10)
& sK9 != sK10
& sK13 = sK15
& organization(sK4,sK14)
& organization(sK5,sK14)
& organization(sK4,sK16)
& organization(sK5,sK16)
& class(sK4,sK7,sK14)
& class(sK5,sK7,sK14)
& survival_chance(sK4,sK8,sK14)
& survival_chance(sK5,sK8,sK14)
& reorganization(sK4,sK14,sK15)
& reorganization(sK5,sK14,sK16)
& reorganization_type(sK4,sK6,sK14)
& reorganization_type(sK5,sK6,sK14)
& reorganization_free(sK4,sK15,sK16)
& survival_chance(sK4,sK9,sK13)
& survival_chance(sK5,sK10,sK13)
& complexity(sK4,sK11,sK14)
& complexity(sK5,sK12,sK14)
& greater(sK12,sK11)
& ( greater(sK9,sK10)
| sK13 != sK16 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6),skolemize(X3,sK7),skolemize(X4,sK8),skolemize(X5,sK9),skolemize(X6,sK10),skolemize(X7,sK11),skolemize(X8,sK12),skolemize(X9,sK13),skolemize(X10,sK14),skolemize(X11,sK15),skolemize(X12,sK16)],[f36]) ).
fof(f45,plain,
! [X2,X3,X0,X1] :
( ~ organization(X0,X2)
| organization(X0,X1)
| ~ organization(X0,X3)
| ~ greater(X1,X2)
| ~ greater(X3,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ reorganization(X0,X1,X2)
| greater(X2,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f49,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ organization(X0,X6)
| greater(X8,X7)
| ~ organization(X1,X6)
| ~ organization(X1,X8)
| ~ class(X0,X3,X6)
| ~ class(X1,X3,X6)
| ~ reorganization(X0,X6,X7)
| ~ reorganization(X1,X6,X8)
| ~ reorganization_type(X0,X2,X6)
| ~ reorganization_type(X1,X2,X6)
| ~ complexity(X0,X4,X6)
| ~ complexity(X1,X5,X6)
| ~ greater(X5,X4) ),
inference(cnf_transformation,[],[f30]) ).
fof(f50,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ organization(X0,X9)
| X5 = X6
| greater(X5,X6)
| ~ organization(X1,X9)
| ~ organization(X0,X10)
| ~ organization(X1,X10)
| ~ class(X0,X3,X9)
| ~ class(X1,X3,X9)
| ~ survival_chance(X0,X4,X9)
| ~ survival_chance(X1,X4,X9)
| ~ reorganization(X0,X9,X10)
| ~ reorganization(X1,X9,X11)
| ~ reorganization_type(X0,X2,X9)
| ~ reorganization_type(X1,X2,X9)
| ~ survival_chance(X0,X5,X10)
| ~ survival_chance(X1,X6,X10)
| ~ complexity(X0,X7,X9)
| ~ complexity(X1,X8,X9)
| ~ greater(X8,X7) ),
inference(cnf_transformation,[],[f32]) ).
fof(f57,plain,
greater(sK12,sK11),
inference(cnf_transformation,[],[f39]) ).
fof(f58,plain,
complexity(sK5,sK12,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f59,plain,
complexity(sK4,sK11,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f60,plain,
survival_chance(sK5,sK10,sK13),
inference(cnf_transformation,[],[f39]) ).
fof(f61,plain,
survival_chance(sK4,sK9,sK13),
inference(cnf_transformation,[],[f39]) ).
fof(f63,plain,
reorganization_type(sK5,sK6,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f64,plain,
reorganization_type(sK4,sK6,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f65,plain,
reorganization(sK5,sK14,sK16),
inference(cnf_transformation,[],[f39]) ).
fof(f66,plain,
reorganization(sK4,sK14,sK15),
inference(cnf_transformation,[],[f39]) ).
fof(f67,plain,
survival_chance(sK5,sK8,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f68,plain,
survival_chance(sK4,sK8,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f69,plain,
class(sK5,sK7,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f70,plain,
class(sK4,sK7,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f71,plain,
organization(sK5,sK16),
inference(cnf_transformation,[],[f39]) ).
fof(f72,plain,
organization(sK4,sK16),
inference(cnf_transformation,[],[f39]) ).
fof(f73,plain,
organization(sK5,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f74,plain,
organization(sK4,sK14),
inference(cnf_transformation,[],[f39]) ).
fof(f75,plain,
sK13 = sK15,
inference(cnf_transformation,[],[f39]) ).
fof(f76,plain,
sK9 != sK10,
inference(cnf_transformation,[],[f39]) ).
fof(f77,plain,
~ greater(sK9,sK10),
inference(cnf_transformation,[],[f39]) ).
fof(f78,plain,
survival_chance(sK4,sK9,sK15),
inference(definition_unfolding,[],[f61,f75]) ).
fof(f79,plain,
survival_chance(sK5,sK10,sK15),
inference(definition_unfolding,[],[f60,f75]) ).
fof(f86,definition,
( spl17_2
<=> greater(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl17_2])],[avatar_definition]) ).
fof(f87,plain,
( ~ greater(sK9,sK10)
| spl17_2 ),
inference(avatar_component_clause,[],[f86]) ).
fof(f90,plain,
~ spl17_2,
inference(avatar_split_clause,[],[f77,f86]) ).
fof(f94,plain,
greater(sK15,sK14),
inference(resolution,[],[f46,f66]) ).
fof(f108,plain,
! [X0,X1] :
( ~ organization(sK5,X1)
| organization(sK5,X0)
| ~ greater(X0,sK14)
| ~ greater(X1,X0) ),
inference(resolution,[],[f45,f73]) ).
fof(f109,plain,
! [X0,X1] :
( ~ organization(sK4,X1)
| organization(sK4,X0)
| ~ greater(X0,sK14)
| ~ greater(X1,X0) ),
inference(resolution,[],[f45,f74]) ).
fof(f144,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ organization(X2,sK14)
| greater(X0,X1)
| ~ organization(X2,X0)
| ~ class(sK4,X3,sK14)
| ~ class(X2,X3,sK14)
| ~ reorganization(sK4,sK14,X1)
| ~ reorganization(X2,sK14,X0)
| ~ reorganization_type(sK4,X4,sK14)
| ~ reorganization_type(X2,X4,sK14)
| ~ complexity(sK4,X5,sK14)
| ~ complexity(X2,X6,sK14)
| ~ greater(X6,X5) ),
inference(resolution,[],[f49,f74]) ).
fof(f148,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ organization(X2,sK14)
| greater(X0,X1)
| X0 = X1
| ~ organization(sK4,X3)
| ~ organization(X2,X3)
| ~ class(sK4,X4,sK14)
| ~ class(X2,X4,sK14)
| ~ survival_chance(sK4,X5,sK14)
| ~ survival_chance(X2,X5,sK14)
| ~ reorganization(sK4,sK14,X3)
| ~ reorganization(X2,sK14,X6)
| ~ reorganization_type(sK4,X7,sK14)
| ~ reorganization_type(X2,X7,sK14)
| ~ survival_chance(sK4,X0,X3)
| ~ survival_chance(X2,X1,X3)
| ~ complexity(sK4,X8,sK14)
| ~ complexity(X2,X9,sK14)
| ~ greater(X9,X8) ),
inference(resolution,[],[f50,f74]) ).
fof(f153,plain,
! [X0] :
( ~ greater(X0,sK14)
| organization(sK5,X0)
| ~ greater(sK16,X0) ),
inference(resolution,[],[f108,f71]) ).
fof(f155,plain,
! [X0] :
( ~ greater(X0,sK14)
| organization(sK4,X0)
| ~ greater(sK16,X0) ),
inference(resolution,[],[f109,f72]) ).
fof(f158,plain,
( organization(sK5,sK15)
| ~ greater(sK16,sK15) ),
inference(resolution,[],[f153,f94]) ).
fof(f160,definition,
( spl17_3
<=> greater(sK16,sK15) ),
introduced(definition,[new_symbols(definition,[spl17_3])],[avatar_definition]) ).
fof(f161,plain,
( greater(sK16,sK15)
| ~ spl17_3 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f162,plain,
( ~ greater(sK16,sK15)
| spl17_3 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f164,definition,
( spl17_4
<=> organization(sK5,sK15) ),
introduced(definition,[new_symbols(definition,[spl17_4])],[avatar_definition]) ).
fof(f166,plain,
( organization(sK5,sK15)
| ~ spl17_4 ),
inference(avatar_component_clause,[],[f164]) ).
fof(f167,plain,
( ~ spl17_3
| spl17_4 ),
inference(avatar_split_clause,[],[f158,f164,f160]) ).
fof(f282,plain,
( organization(sK4,sK15)
| ~ greater(sK16,sK15) ),
inference(resolution,[],[f155,f94]) ).
fof(f421,definition,
( spl17_48
<=> ! [X3] :
( ~ reorganization_type(sK5,X3,sK14)
| ~ reorganization_type(sK4,X3,sK14) ) ),
introduced(definition,[new_symbols(definition,[spl17_48])],[avatar_definition]) ).
fof(f422,plain,
( ! [X3] :
( ~ reorganization_type(sK5,X3,sK14)
| ~ reorganization_type(sK4,X3,sK14) )
| ~ spl17_48 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f424,definition,
( spl17_49
<=> ! [X2] :
( ~ class(sK5,X2,sK14)
| ~ class(sK4,X2,sK14) ) ),
introduced(definition,[new_symbols(definition,[spl17_49])],[avatar_definition]) ).
fof(f425,plain,
( ! [X2] :
( ~ class(sK5,X2,sK14)
| ~ class(sK4,X2,sK14) )
| ~ spl17_49 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f446,plain,
! [X2,X3,X0,X1,X4,X5] :
( greater(X0,X1)
| ~ organization(sK5,X0)
| ~ class(sK4,X2,sK14)
| ~ class(sK5,X2,sK14)
| ~ reorganization(sK4,sK14,X1)
| ~ reorganization(sK5,sK14,X0)
| ~ reorganization_type(sK4,X3,sK14)
| ~ reorganization_type(sK5,X3,sK14)
| ~ complexity(sK4,X4,sK14)
| ~ complexity(sK5,X5,sK14)
| ~ greater(X5,X4) ),
inference(resolution,[],[f144,f73]) ).
fof(f463,definition,
( spl17_59
<=> ! [X4,X5] :
( ~ complexity(sK4,X4,sK14)
| ~ complexity(sK5,X5,sK14)
| ~ greater(X5,X4) ) ),
introduced(definition,[new_symbols(definition,[spl17_59])],[avatar_definition]) ).
fof(f464,plain,
( ! [X4,X5] :
( ~ greater(X5,X4)
| ~ complexity(sK5,X5,sK14)
| ~ complexity(sK4,X4,sK14) )
| ~ spl17_59 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f466,definition,
( spl17_60
<=> ! [X0,X1] :
( greater(X0,X1)
| ~ reorganization(sK5,sK14,X0)
| ~ reorganization(sK4,sK14,X1)
| ~ organization(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl17_60])],[avatar_definition]) ).
fof(f467,plain,
( ! [X0,X1] :
( ~ organization(sK5,X0)
| ~ reorganization(sK5,sK14,X0)
| ~ reorganization(sK4,sK14,X1)
| greater(X0,X1) )
| ~ spl17_60 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f468,plain,
( spl17_59
| spl17_48
| spl17_49
| spl17_60 ),
inference(avatar_split_clause,[],[f446,f466,f424,f421,f463]) ).
fof(f491,plain,
( ~ reorganization_type(sK4,sK6,sK14)
| ~ spl17_48 ),
inference(resolution,[],[f422,f63]) ).
fof(f492,plain,
( $false
| ~ spl17_48 ),
inference(forward_subsumption_resolution,[],[f491,f64]) ).
fof(f493,plain,
~ spl17_48,
inference(avatar_contradiction_clause,[],[f492]) ).
fof(f494,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( greater(X0,X1)
| X0 = X1
| ~ organization(sK4,X2)
| ~ organization(sK5,X2)
| ~ class(sK4,X3,sK14)
| ~ class(sK5,X3,sK14)
| ~ survival_chance(sK4,X4,sK14)
| ~ survival_chance(sK5,X4,sK14)
| ~ reorganization(sK4,sK14,X2)
| ~ reorganization(sK5,sK14,X5)
| ~ reorganization_type(sK4,X6,sK14)
| ~ reorganization_type(sK5,X6,sK14)
| ~ survival_chance(sK4,X0,X2)
| ~ survival_chance(sK5,X1,X2)
| ~ complexity(sK4,X7,sK14)
| ~ complexity(sK5,X8,sK14)
| ~ greater(X8,X7) ),
inference(resolution,[],[f148,f73]) ).
fof(f497,plain,
( ~ class(sK4,sK7,sK14)
| ~ spl17_49 ),
inference(resolution,[],[f425,f69]) ).
fof(f498,plain,
( $false
| ~ spl17_49 ),
inference(forward_subsumption_resolution,[],[f497,f70]) ).
fof(f499,plain,
~ spl17_49,
inference(avatar_contradiction_clause,[],[f498]) ).
fof(f654,plain,
( ~ complexity(sK5,sK12,sK14)
| ~ complexity(sK4,sK11,sK14)
| ~ spl17_59 ),
inference(resolution,[],[f464,f57]) ).
fof(f657,plain,
( ~ complexity(sK4,sK11,sK14)
| ~ spl17_59 ),
inference(forward_subsumption_resolution,[],[f654,f58]) ).
fof(f663,plain,
( $false
| ~ spl17_59 ),
inference(forward_subsumption_resolution,[],[f657,f59]) ).
fof(f664,plain,
~ spl17_59,
inference(avatar_contradiction_clause,[],[f663]) ).
fof(f666,definition,
( spl17_87
<=> ! [X5] : ~ reorganization(sK5,sK14,X5) ),
introduced(definition,[new_symbols(definition,[spl17_87])],[avatar_definition]) ).
fof(f667,plain,
( ! [X5] : ~ reorganization(sK5,sK14,X5)
| ~ spl17_87 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f669,definition,
( spl17_88
<=> ! [X4] :
( ~ survival_chance(sK4,X4,sK14)
| ~ survival_chance(sK5,X4,sK14) ) ),
introduced(definition,[new_symbols(definition,[spl17_88])],[avatar_definition]) ).
fof(f670,plain,
( ! [X4] :
( ~ survival_chance(sK5,X4,sK14)
| ~ survival_chance(sK4,X4,sK14) )
| ~ spl17_88 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,definition,
( spl17_89
<=> ! [X2,X0,X1] :
( greater(X0,X1)
| ~ survival_chance(sK5,X1,X2)
| ~ survival_chance(sK4,X0,X2)
| ~ organization(sK4,X2)
| ~ reorganization(sK4,sK14,X2)
| ~ organization(sK5,X2)
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl17_89])],[avatar_definition]) ).
fof(f673,plain,
( ! [X2,X0,X1] :
( ~ organization(sK5,X2)
| ~ survival_chance(sK5,X1,X2)
| ~ survival_chance(sK4,X0,X2)
| ~ organization(sK4,X2)
| ~ reorganization(sK4,sK14,X2)
| greater(X0,X1)
| X0 = X1 )
| ~ spl17_89 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f674,plain,
( spl17_59
| spl17_48
| spl17_87
| spl17_88
| spl17_49
| spl17_89 ),
inference(avatar_split_clause,[],[f494,f672,f424,f669,f666,f421,f463]) ).
fof(f675,plain,
( $false
| ~ spl17_87 ),
inference(resolution,[],[f667,f65]) ).
fof(f676,plain,
~ spl17_87,
inference(avatar_contradiction_clause,[],[f675]) ).
fof(f678,plain,
( ~ survival_chance(sK4,sK8,sK14)
| ~ spl17_88 ),
inference(resolution,[],[f670,f67]) ).
fof(f679,plain,
( $false
| ~ spl17_88 ),
inference(forward_subsumption_resolution,[],[f678,f68]) ).
fof(f680,plain,
~ spl17_88,
inference(avatar_contradiction_clause,[],[f679]) ).
fof(f684,plain,
( ! [X0] :
( ~ reorganization(sK5,sK14,sK16)
| ~ reorganization(sK4,sK14,X0)
| greater(sK16,X0) )
| ~ spl17_60 ),
inference(resolution,[],[f467,f71]) ).
fof(f694,plain,
( ! [X0] :
( ~ reorganization(sK4,sK14,X0)
| greater(sK16,X0) )
| ~ spl17_60 ),
inference(forward_subsumption_resolution,[],[f684,f65]) ).
fof(f762,plain,
( greater(sK16,sK15)
| ~ spl17_60 ),
inference(resolution,[],[f694,f66]) ).
fof(f763,plain,
( $false
| spl17_3
| ~ spl17_60 ),
inference(forward_subsumption_resolution,[],[f762,f162]) ).
fof(f764,plain,
( spl17_3
| ~ spl17_60 ),
inference(avatar_contradiction_clause,[],[f763]) ).
fof(f765,plain,
( organization(sK4,sK15)
| ~ spl17_3 ),
inference(forward_subsumption_resolution,[],[f282,f161]) ).
fof(f831,plain,
( ! [X0,X1] :
( ~ survival_chance(sK5,X0,sK15)
| ~ survival_chance(sK4,X1,sK15)
| ~ organization(sK4,sK15)
| ~ reorganization(sK4,sK14,sK15)
| greater(X1,X0)
| X0 = X1 )
| ~ spl17_4
| ~ spl17_89 ),
inference(resolution,[],[f166,f673]) ).
fof(f838,plain,
( ! [X0,X1] :
( ~ survival_chance(sK5,X0,sK15)
| ~ survival_chance(sK4,X1,sK15)
| ~ reorganization(sK4,sK14,sK15)
| greater(X1,X0)
| X0 = X1 )
| ~ spl17_3
| ~ spl17_4
| ~ spl17_89 ),
inference(forward_subsumption_resolution,[],[f831,f765]) ).
fof(f849,plain,
( ! [X0,X1] :
( ~ survival_chance(sK5,X0,sK15)
| ~ survival_chance(sK4,X1,sK15)
| greater(X1,X0)
| X0 = X1 )
| ~ spl17_3
| ~ spl17_4
| ~ spl17_89 ),
inference(forward_subsumption_resolution,[],[f838,f66]) ).
fof(f1481,plain,
( ! [X0] :
( ~ survival_chance(sK4,X0,sK15)
| greater(X0,sK10)
| sK10 = X0 )
| ~ spl17_3
| ~ spl17_4
| ~ spl17_89 ),
inference(resolution,[],[f849,f79]) ).
fof(f1485,plain,
( greater(sK9,sK10)
| sK9 = sK10
| ~ spl17_3
| ~ spl17_4
| ~ spl17_89 ),
inference(resolution,[],[f1481,f78]) ).
fof(f1487,plain,
( sK9 = sK10
| spl17_2
| ~ spl17_3
| ~ spl17_4
| ~ spl17_89 ),
inference(forward_subsumption_resolution,[],[f1485,f87]) ).
fof(f1488,plain,
( $false
| spl17_2
| ~ spl17_3
| ~ spl17_4
| ~ spl17_89 ),
inference(forward_subsumption_resolution,[],[f1487,f76]) ).
fof(f1489,plain,
( spl17_2
| ~ spl17_3
| ~ spl17_4
| ~ spl17_89 ),
inference(avatar_contradiction_clause,[],[f1488]) ).
cnf(s2,plain,
~ spl17_2,
inference(sat_conversion,[],[f90]) ).
cnf(s3,plain,
( ~ spl17_3
| spl17_4 ),
inference(sat_conversion,[],[f167]) ).
cnf(s28,plain,
( spl17_48
| spl17_49
| spl17_59
| spl17_60 ),
inference(sat_conversion,[],[f468]) ).
cnf(s29,plain,
~ spl17_48,
inference(sat_conversion,[],[f493]) ).
cnf(s30,plain,
~ spl17_49,
inference(sat_conversion,[],[f499]) ).
cnf(s52,plain,
~ spl17_59,
inference(sat_conversion,[],[f664]) ).
cnf(s53,plain,
( spl17_48
| spl17_49
| spl17_59
| spl17_87
| spl17_88
| spl17_89 ),
inference(sat_conversion,[],[f674]) ).
cnf(s54,plain,
~ spl17_87,
inference(sat_conversion,[],[f676]) ).
cnf(s55,plain,
~ spl17_88,
inference(sat_conversion,[],[f680]) ).
cnf(s61,plain,
( spl17_3
| ~ spl17_60 ),
inference(sat_conversion,[],[f764]) ).
cnf(s97,plain,
( spl17_2
| ~ spl17_3
| ~ spl17_4
| ~ spl17_89 ),
inference(sat_conversion,[],[f1489]) ).
cnf(s102,plain,
( spl17_48
| spl17_49
| spl17_59
| spl17_89 ),
inference(rat,[],[s53,s55,s54]) ).
cnf(s103,plain,
spl17_89,
inference(rat,[],[s102,s30,s52,s29]) ).
cnf(s104,plain,
spl17_60,
inference(rat,[],[s28,s52,s30,s29]) ).
cnf(s105,plain,
spl17_3,
inference(rat,[],[s61,s104]) ).
cnf(s111,plain,
spl17_4,
inference(rat,[],[s3,s105]) ).
cnf(s113,plain,
spl17_2,
inference(rat,[],[s97,s103,s105,s111]) ).
cnf(s114,plain,
$false,
inference(rat,[],[s2,s113]) ).
fof(f1490,plain,
$false,
inference(avatar_sat_refutation,[],[s114]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n004.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 17:15:37 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.39 Running first-order model finding
% 0.09/0.39 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
% 0.09/0.45 % (3766384)Will run a generic schedule for satisfiability detection.
% 0.09/0.45 % (3766394)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=168727139:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.09/0.45 % (3766390)% WARNING: option uhcvi not known.
% 0.09/0.45 % (3766389)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3494576397_2999 on theBenchmark for (2999ds/0Mi)
% 0.09/0.45 % (3766391)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2253363994:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.09/0.45 % (3766392)dis+10_1_sil=32000:sp=arity:random_seed=2106507010:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.09/0.45 % (3766393)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1270530618:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.09/0.45 % (3766390)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3703603972:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.09/0.45 % (3766395)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2051210105:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.09/0.45 % TRYING [1]
% 0.09/0.45 % TRYING [2]
% 0.09/0.45 % TRYING [3]
% 0.09/0.45 % (3766394) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3766384-3766394"...
% 0.09/0.45 % (3766394)...printing done.
% 0.09/0.45 % (3766394)Refutation found. Thanks to Tanya!
% 0.09/0.45 % SZS status Theorem for theBenchmark
% 0.09/0.45 % SZS output start Proof for theBenchmark
% See solution above
% 0.09/0.45 % (3766394)------------------------------
% 0.09/0.45 % (3766394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.45 % (3766394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.45 % (3766394)CaDiCaL version: 2.1.3
% 0.09/0.45 % (3766394)Termination reason: Refutation
% 0.09/0.45 % (3766394)Time elapsed: 0.024 s
% 0.09/0.45 % (3766394)Peak memory usage: 13 MB
% 0.09/0.45 % (3766394)Instructions burned: 75 (million)
% 0.09/0.45 % (3766384)Success in time 0.05 s
% 0.09/0.45 % Vampire exiting
%------------------------------------------------------------------------------