%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MGT005+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:26 PM UTC 2026
% Result : Theorem 0.37s 0.47s
% Output : Refutation 0.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 24
% Syntax : Number of formulae : 188 ( 43 unt; 14 def)
% Number of atoms : 805 ( 15 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 1070 ( 453 ~; 461 |; 132 &)
% ( 14 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 15 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 12 con; 0-2 aty)
% Number of variables : 336 ( 0 sgn 310 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] :
~ ( greater(X0,X1)
& greater(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp6_2) ).
fof(f3,axiom,
! [X0,X1,X2] :
( ( greater(X0,X1)
& greater(X1,X2) )
=> greater(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp11) ).
fof(f4,axiom,
! [X0,X1] :
( organization(X0,X1)
=> ? [X2] : survival_chance(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp12) ).
fof(f5,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(f6,axiom,
! [X0,X1,X2] :
( reorganization(X0,X1,X2)
=> greater(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp7) ).
fof(f7,axiom,
! [X0,X1,X2,X3,X4] :
( ( organization(X0,X3)
& organization(X0,X4)
& reorganization_free(X0,X3,X4)
& survival_chance(X0,X1,X3)
& survival_chance(X0,X2,X4)
& greater(X4,X3) )
=> greater(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_FOL) ).
fof(f8,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( organization(X0,X3)
& organization(X0,X4)
& reorganization(X0,X5,X6)
& survival_chance(X0,X1,X3)
& survival_chance(X0,X2,X4)
& ~ greater(X5,X3)
& greater(X4,X3)
& ~ greater(X4,X6) )
=> greater(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_FOL) ).
fof(f9,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(f10,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(f11,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( organization(X0,X9)
& organization(X1,X9)
& organization(X0,X11)
& organization(X1,X11)
& 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)
& reorganization_free(X0,X10,X11)
& survival_chance(X0,X5,X11)
& survival_chance(X1,X6,X11)
& complexity(X0,X7,X9)
& complexity(X1,X8,X9)
& greater(X8,X7) )
=> greater(X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL) ).
fof(f12,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( organization(X0,X9)
& organization(X1,X9)
& organization(X0,X11)
& organization(X1,X11)
& 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)
& reorganization_free(X0,X10,X11)
& survival_chance(X0,X5,X11)
& survival_chance(X1,X6,X11)
& complexity(X0,X7,X9)
& complexity(X1,X8,X9)
& greater(X8,X7) )
=> greater(X5,X6) ),
inference(negated_conjecture,[status(cth)],[f11]) ).
fof(f14,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| ~ greater(X1,X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f15,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f16,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(flattening,[],[f15]) ).
fof(f17,plain,
! [X0,X1] :
( ? [X2] : survival_chance(X0,X2,X1)
| ~ organization(X0,X1) ),
inference(ennf_transformation,[],[f4]) ).
fof(f18,plain,
! [X0,X1,X2,X3] :
( organization(X0,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X3)
| ~ greater(X1,X2)
| ~ greater(X3,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f19,plain,
! [X0,X1,X2,X3] :
( organization(X0,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X3)
| ~ greater(X1,X2)
| ~ greater(X3,X1) ),
inference(flattening,[],[f18]) ).
fof(f20,plain,
! [X0,X1,X2] :
( greater(X2,X1)
| ~ reorganization(X0,X1,X2) ),
inference(ennf_transformation,[],[f6]) ).
fof(f21,plain,
! [X0,X1,X2,X3,X4] :
( greater(X2,X1)
| ~ organization(X0,X3)
| ~ organization(X0,X4)
| ~ reorganization_free(X0,X3,X4)
| ~ survival_chance(X0,X1,X3)
| ~ survival_chance(X0,X2,X4)
| ~ greater(X4,X3) ),
inference(ennf_transformation,[],[f7]) ).
fof(f22,plain,
! [X0,X1,X2,X3,X4] :
( greater(X2,X1)
| ~ organization(X0,X3)
| ~ organization(X0,X4)
| ~ reorganization_free(X0,X3,X4)
| ~ survival_chance(X0,X1,X3)
| ~ survival_chance(X0,X2,X4)
| ~ greater(X4,X3) ),
inference(flattening,[],[f21]) ).
fof(f23,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( greater(X1,X2)
| ~ organization(X0,X3)
| ~ organization(X0,X4)
| ~ reorganization(X0,X5,X6)
| ~ survival_chance(X0,X1,X3)
| ~ survival_chance(X0,X2,X4)
| greater(X5,X3)
| ~ greater(X4,X3)
| greater(X4,X6) ),
inference(ennf_transformation,[],[f8]) ).
fof(f24,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( greater(X1,X2)
| ~ organization(X0,X3)
| ~ organization(X0,X4)
| ~ reorganization(X0,X5,X6)
| ~ survival_chance(X0,X1,X3)
| ~ survival_chance(X0,X2,X4)
| greater(X5,X3)
| ~ greater(X4,X3)
| greater(X4,X6) ),
inference(flattening,[],[f23]) ).
fof(f25,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,[],[f9]) ).
fof(f26,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,[],[f25]) ).
fof(f27,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,[],[f10]) ).
fof(f28,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,[],[f27]) ).
fof(f29,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ greater(X5,X6)
& organization(X0,X9)
& organization(X1,X9)
& organization(X0,X11)
& organization(X1,X11)
& 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)
& reorganization_free(X0,X10,X11)
& survival_chance(X0,X5,X11)
& survival_chance(X1,X6,X11)
& complexity(X0,X7,X9)
& complexity(X1,X8,X9)
& greater(X8,X7) ),
inference(ennf_transformation,[],[f12]) ).
fof(f30,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ greater(X5,X6)
& organization(X0,X9)
& organization(X1,X9)
& organization(X0,X11)
& organization(X1,X11)
& 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)
& reorganization_free(X0,X10,X11)
& survival_chance(X0,X5,X11)
& survival_chance(X1,X6,X11)
& complexity(X0,X7,X9)
& complexity(X1,X8,X9)
& greater(X8,X7) ),
inference(flattening,[],[f29]) ).
fof(f31,plain,
! [X0,X1] :
( survival_chance(X0,sK0(X0,X1),X1)
| ~ organization(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f17]) ).
fof(f32,plain,
( ~ greater(sK6,sK7)
& organization(sK1,sK10)
& organization(sK2,sK10)
& organization(sK1,sK12)
& organization(sK2,sK12)
& class(sK1,sK4,sK10)
& class(sK2,sK4,sK10)
& survival_chance(sK1,sK5,sK10)
& survival_chance(sK2,sK5,sK10)
& reorganization(sK1,sK10,sK11)
& reorganization(sK2,sK10,sK12)
& reorganization_type(sK1,sK3,sK10)
& reorganization_type(sK2,sK3,sK10)
& reorganization_free(sK1,sK11,sK12)
& survival_chance(sK1,sK6,sK12)
& survival_chance(sK2,sK7,sK12)
& complexity(sK1,sK8,sK10)
& complexity(sK2,sK9,sK10)
& greater(sK9,sK8) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X4,sK5),skolemize(X5,sK6),skolemize(X6,sK7),skolemize(X7,sK8),skolemize(X8,sK9),skolemize(X9,sK10),skolemize(X10,sK11),skolemize(X11,sK12)],[f30]) ).
fof(f34,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| ~ greater(X1,X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f35,plain,
! [X2,X0,X1] :
( ~ greater(X0,X1)
| greater(X0,X2)
| ~ greater(X1,X2) ),
inference(cnf_transformation,[],[f16]) ).
fof(f36,plain,
! [X0,X1] :
( ~ organization(X0,X1)
| survival_chance(X0,sK0(X0,X1),X1) ),
inference(cnf_transformation,[],[f31]) ).
fof(f37,plain,
! [X2,X3,X0,X1] :
( ~ organization(X0,X2)
| organization(X0,X1)
| ~ organization(X0,X3)
| ~ greater(X1,X2)
| ~ greater(X3,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f38,plain,
! [X2,X0,X1] :
( ~ reorganization(X0,X1,X2)
| greater(X2,X1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f39,plain,
! [X2,X3,X0,X1,X4] :
( ~ organization(X0,X3)
| greater(X2,X1)
| ~ organization(X0,X4)
| ~ reorganization_free(X0,X3,X4)
| ~ survival_chance(X0,X1,X3)
| ~ survival_chance(X0,X2,X4)
| ~ greater(X4,X3) ),
inference(cnf_transformation,[],[f22]) ).
fof(f40,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ organization(X0,X3)
| greater(X1,X2)
| ~ organization(X0,X4)
| ~ reorganization(X0,X5,X6)
| ~ survival_chance(X0,X1,X3)
| ~ survival_chance(X0,X2,X4)
| greater(X5,X3)
| ~ greater(X4,X3)
| greater(X4,X6) ),
inference(cnf_transformation,[],[f24]) ).
fof(f41,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,[],[f26]) ).
fof(f42,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,[],[f28]) ).
fof(f43,plain,
greater(sK9,sK8),
inference(cnf_transformation,[],[f32]) ).
fof(f44,plain,
complexity(sK2,sK9,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f45,plain,
complexity(sK1,sK8,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f46,plain,
survival_chance(sK2,sK7,sK12),
inference(cnf_transformation,[],[f32]) ).
fof(f47,plain,
survival_chance(sK1,sK6,sK12),
inference(cnf_transformation,[],[f32]) ).
fof(f48,plain,
reorganization_free(sK1,sK11,sK12),
inference(cnf_transformation,[],[f32]) ).
fof(f49,plain,
reorganization_type(sK2,sK3,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f50,plain,
reorganization_type(sK1,sK3,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f51,plain,
reorganization(sK2,sK10,sK12),
inference(cnf_transformation,[],[f32]) ).
fof(f52,plain,
reorganization(sK1,sK10,sK11),
inference(cnf_transformation,[],[f32]) ).
fof(f53,plain,
survival_chance(sK2,sK5,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f54,plain,
survival_chance(sK1,sK5,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f55,plain,
class(sK2,sK4,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f56,plain,
class(sK1,sK4,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f57,plain,
organization(sK2,sK12),
inference(cnf_transformation,[],[f32]) ).
fof(f58,plain,
organization(sK1,sK12),
inference(cnf_transformation,[],[f32]) ).
fof(f59,plain,
organization(sK2,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f60,plain,
organization(sK1,sK10),
inference(cnf_transformation,[],[f32]) ).
fof(f61,plain,
~ greater(sK6,sK7),
inference(cnf_transformation,[],[f32]) ).
fof(f65,plain,
greater(sK11,sK10),
inference(resolution,[],[f38,f52]) ).
fof(f71,plain,
~ greater(sK10,sK11),
inference(resolution,[],[f65,f34]) ).
fof(f79,plain,
! [X0,X1] :
( ~ organization(sK2,X1)
| organization(sK2,X0)
| ~ greater(X0,sK10)
| ~ greater(X1,X0) ),
inference(resolution,[],[f37,f59]) ).
fof(f80,plain,
! [X0,X1] :
( ~ organization(sK1,X1)
| organization(sK1,X0)
| ~ greater(X0,sK10)
| ~ greater(X1,X0) ),
inference(resolution,[],[f37,f60]) ).
fof(f92,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ organization(X2,sK10)
| greater(X0,X1)
| ~ organization(X2,X0)
| ~ class(sK1,X3,sK10)
| ~ class(X2,X3,sK10)
| ~ reorganization(sK1,sK10,X1)
| ~ reorganization(X2,sK10,X0)
| ~ reorganization_type(sK1,X4,sK10)
| ~ reorganization_type(X2,X4,sK10)
| ~ complexity(sK1,X5,sK10)
| ~ complexity(X2,X6,sK10)
| ~ greater(X6,X5) ),
inference(resolution,[],[f41,f60]) ).
fof(f96,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ organization(X2,sK10)
| greater(X0,X1)
| X0 = X1
| ~ organization(sK1,X3)
| ~ organization(X2,X3)
| ~ class(sK1,X4,sK10)
| ~ class(X2,X4,sK10)
| ~ survival_chance(sK1,X5,sK10)
| ~ survival_chance(X2,X5,sK10)
| ~ reorganization(sK1,sK10,X3)
| ~ reorganization(X2,sK10,X6)
| ~ reorganization_type(sK1,X7,sK10)
| ~ reorganization_type(X2,X7,sK10)
| ~ survival_chance(sK1,X0,X3)
| ~ survival_chance(X2,X1,X3)
| ~ complexity(sK1,X8,sK10)
| ~ complexity(X2,X9,sK10)
| ~ greater(X9,X8) ),
inference(resolution,[],[f42,f60]) ).
fof(f101,plain,
! [X0] :
( ~ greater(X0,sK10)
| organization(sK2,X0)
| ~ greater(sK12,X0) ),
inference(resolution,[],[f79,f57]) ).
fof(f103,plain,
! [X0] :
( ~ greater(X0,sK10)
| organization(sK1,X0)
| ~ greater(sK12,X0) ),
inference(resolution,[],[f80,f58]) ).
fof(f106,plain,
( organization(sK2,sK11)
| ~ greater(sK12,sK11) ),
inference(resolution,[],[f101,f65]) ).
fof(f108,definition,
( spl13_1
<=> greater(sK12,sK11) ),
introduced(definition,[new_symbols(definition,[spl13_1])],[avatar_definition]) ).
fof(f109,plain,
( greater(sK12,sK11)
| ~ spl13_1 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f110,plain,
( ~ greater(sK12,sK11)
| spl13_1 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f112,definition,
( spl13_2
<=> organization(sK2,sK11) ),
introduced(definition,[new_symbols(definition,[spl13_2])],[avatar_definition]) ).
fof(f114,plain,
( organization(sK2,sK11)
| ~ spl13_2 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,plain,
( ~ spl13_1
| spl13_2 ),
inference(avatar_split_clause,[],[f106,f112,f108]) ).
fof(f119,definition,
( spl13_3
<=> greater(sK12,sK12) ),
introduced(definition,[new_symbols(definition,[spl13_3])],[avatar_definition]) ).
fof(f120,plain,
( greater(sK12,sK12)
| ~ spl13_3 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f121,plain,
( ~ greater(sK12,sK12)
| spl13_3 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f171,plain,
( organization(sK1,sK11)
| ~ greater(sK12,sK11) ),
inference(resolution,[],[f103,f65]) ).
fof(f293,definition,
( spl13_40
<=> ! [X3] :
( ~ reorganization_type(sK2,X3,sK10)
| ~ reorganization_type(sK1,X3,sK10) ) ),
introduced(definition,[new_symbols(definition,[spl13_40])],[avatar_definition]) ).
fof(f294,plain,
( ! [X3] :
( ~ reorganization_type(sK2,X3,sK10)
| ~ reorganization_type(sK1,X3,sK10) )
| ~ spl13_40 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f296,definition,
( spl13_41
<=> ! [X2] :
( ~ class(sK2,X2,sK10)
| ~ class(sK1,X2,sK10) ) ),
introduced(definition,[new_symbols(definition,[spl13_41])],[avatar_definition]) ).
fof(f297,plain,
( ! [X2] :
( ~ class(sK2,X2,sK10)
| ~ class(sK1,X2,sK10) )
| ~ spl13_41 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f315,plain,
! [X2,X3,X0,X1,X4,X5] :
( greater(X0,X1)
| ~ organization(sK2,X0)
| ~ class(sK1,X2,sK10)
| ~ class(sK2,X2,sK10)
| ~ reorganization(sK1,sK10,X1)
| ~ reorganization(sK2,sK10,X0)
| ~ reorganization_type(sK1,X3,sK10)
| ~ reorganization_type(sK2,X3,sK10)
| ~ complexity(sK1,X4,sK10)
| ~ complexity(sK2,X5,sK10)
| ~ greater(X5,X4) ),
inference(resolution,[],[f92,f59]) ).
fof(f332,definition,
( spl13_51
<=> ! [X4,X5] :
( ~ complexity(sK1,X4,sK10)
| ~ complexity(sK2,X5,sK10)
| ~ greater(X5,X4) ) ),
introduced(definition,[new_symbols(definition,[spl13_51])],[avatar_definition]) ).
fof(f333,plain,
( ! [X4,X5] :
( ~ greater(X5,X4)
| ~ complexity(sK2,X5,sK10)
| ~ complexity(sK1,X4,sK10) )
| ~ spl13_51 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f335,definition,
( spl13_52
<=> ! [X0,X1] :
( greater(X0,X1)
| ~ reorganization(sK2,sK10,X0)
| ~ reorganization(sK1,sK10,X1)
| ~ organization(sK2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_52])],[avatar_definition]) ).
fof(f336,plain,
( ! [X0,X1] :
( ~ organization(sK2,X0)
| ~ reorganization(sK2,sK10,X0)
| ~ reorganization(sK1,sK10,X1)
| greater(X0,X1) )
| ~ spl13_52 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f337,plain,
( spl13_51
| spl13_40
| spl13_41
| spl13_52 ),
inference(avatar_split_clause,[],[f315,f335,f296,f293,f332]) ).
fof(f344,plain,
( ~ reorganization_type(sK1,sK3,sK10)
| ~ spl13_40 ),
inference(resolution,[],[f294,f49]) ).
fof(f345,plain,
( $false
| ~ spl13_40 ),
inference(forward_subsumption_resolution,[],[f344,f50]) ).
fof(f346,plain,
~ spl13_40,
inference(avatar_contradiction_clause,[],[f345]) ).
fof(f350,plain,
( ~ class(sK1,sK4,sK10)
| ~ spl13_41 ),
inference(resolution,[],[f297,f55]) ).
fof(f351,plain,
( $false
| ~ spl13_41 ),
inference(forward_subsumption_resolution,[],[f350,f56]) ).
fof(f352,plain,
~ spl13_41,
inference(avatar_contradiction_clause,[],[f351]) ).
fof(f353,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( greater(X0,X1)
| X0 = X1
| ~ organization(sK1,X2)
| ~ organization(sK2,X2)
| ~ class(sK1,X3,sK10)
| ~ class(sK2,X3,sK10)
| ~ survival_chance(sK1,X4,sK10)
| ~ survival_chance(sK2,X4,sK10)
| ~ reorganization(sK1,sK10,X2)
| ~ reorganization(sK2,sK10,X5)
| ~ reorganization_type(sK1,X6,sK10)
| ~ reorganization_type(sK2,X6,sK10)
| ~ survival_chance(sK1,X0,X2)
| ~ survival_chance(sK2,X1,X2)
| ~ complexity(sK1,X7,sK10)
| ~ complexity(sK2,X8,sK10)
| ~ greater(X8,X7) ),
inference(resolution,[],[f96,f59]) ).
fof(f511,plain,
( ~ complexity(sK2,sK9,sK10)
| ~ complexity(sK1,sK8,sK10)
| ~ spl13_51 ),
inference(resolution,[],[f333,f43]) ).
fof(f514,plain,
( ~ complexity(sK1,sK8,sK10)
| ~ spl13_51 ),
inference(forward_subsumption_resolution,[],[f511,f44]) ).
fof(f520,plain,
( $false
| ~ spl13_51 ),
inference(forward_subsumption_resolution,[],[f514,f45]) ).
fof(f521,plain,
~ spl13_51,
inference(avatar_contradiction_clause,[],[f520]) ).
fof(f523,definition,
( spl13_73
<=> ! [X5] : ~ reorganization(sK2,sK10,X5) ),
introduced(definition,[new_symbols(definition,[spl13_73])],[avatar_definition]) ).
fof(f524,plain,
( ! [X5] : ~ reorganization(sK2,sK10,X5)
| ~ spl13_73 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f526,definition,
( spl13_74
<=> ! [X4] :
( ~ survival_chance(sK1,X4,sK10)
| ~ survival_chance(sK2,X4,sK10) ) ),
introduced(definition,[new_symbols(definition,[spl13_74])],[avatar_definition]) ).
fof(f527,plain,
( ! [X4] :
( ~ survival_chance(sK2,X4,sK10)
| ~ survival_chance(sK1,X4,sK10) )
| ~ spl13_74 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f529,definition,
( spl13_75
<=> ! [X2,X0,X1] :
( greater(X0,X1)
| ~ survival_chance(sK2,X1,X2)
| ~ survival_chance(sK1,X0,X2)
| ~ organization(sK1,X2)
| ~ reorganization(sK1,sK10,X2)
| ~ organization(sK2,X2)
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl13_75])],[avatar_definition]) ).
fof(f530,plain,
( ! [X2,X0,X1] :
( ~ organization(sK2,X2)
| ~ survival_chance(sK2,X1,X2)
| ~ survival_chance(sK1,X0,X2)
| ~ organization(sK1,X2)
| ~ reorganization(sK1,sK10,X2)
| greater(X0,X1)
| X0 = X1 )
| ~ spl13_75 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f531,plain,
( spl13_51
| spl13_40
| spl13_73
| spl13_74
| spl13_41
| spl13_75 ),
inference(avatar_split_clause,[],[f353,f529,f296,f526,f523,f293,f332]) ).
fof(f532,plain,
( $false
| ~ spl13_73 ),
inference(resolution,[],[f524,f51]) ).
fof(f533,plain,
~ spl13_73,
inference(avatar_contradiction_clause,[],[f532]) ).
fof(f534,plain,
( ~ survival_chance(sK1,sK5,sK10)
| ~ spl13_74 ),
inference(resolution,[],[f527,f53]) ).
fof(f536,plain,
( $false
| ~ spl13_74 ),
inference(forward_subsumption_resolution,[],[f534,f54]) ).
fof(f537,plain,
~ spl13_74,
inference(avatar_contradiction_clause,[],[f536]) ).
fof(f538,plain,
( ! [X0] :
( ~ reorganization(sK2,sK10,sK12)
| ~ reorganization(sK1,sK10,X0)
| greater(sK12,X0) )
| ~ spl13_52 ),
inference(resolution,[],[f336,f57]) ).
fof(f548,plain,
( ! [X0] :
( ~ reorganization(sK1,sK10,X0)
| greater(sK12,X0) )
| ~ spl13_52 ),
inference(forward_subsumption_resolution,[],[f538,f51]) ).
fof(f611,plain,
( greater(sK12,sK11)
| ~ spl13_52 ),
inference(resolution,[],[f548,f52]) ).
fof(f612,plain,
( $false
| spl13_1
| ~ spl13_52 ),
inference(forward_subsumption_resolution,[],[f611,f110]) ).
fof(f613,plain,
( spl13_1
| ~ spl13_52 ),
inference(avatar_contradiction_clause,[],[f612]) ).
fof(f614,plain,
( organization(sK1,sK11)
| ~ spl13_1 ),
inference(forward_subsumption_resolution,[],[f171,f109]) ).
fof(f653,plain,
( ! [X0,X1] :
( ~ survival_chance(sK2,X0,sK11)
| ~ survival_chance(sK1,X1,sK11)
| ~ organization(sK1,sK11)
| ~ reorganization(sK1,sK10,sK11)
| greater(X1,X0)
| X0 = X1 )
| ~ spl13_2
| ~ spl13_75 ),
inference(resolution,[],[f114,f530]) ).
fof(f656,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ organization(sK2,X2)
| greater(X0,X1)
| ~ reorganization(sK2,X3,X4)
| ~ survival_chance(sK2,X0,sK11)
| ~ survival_chance(sK2,X1,X2)
| greater(X3,sK11)
| ~ greater(X2,sK11)
| greater(X2,X4) )
| ~ spl13_2 ),
inference(resolution,[],[f114,f40]) ).
fof(f659,plain,
( survival_chance(sK2,sK0(sK2,sK11),sK11)
| ~ spl13_2 ),
inference(resolution,[],[f114,f36]) ).
fof(f660,plain,
( ! [X0,X1] :
( ~ survival_chance(sK2,X0,sK11)
| ~ survival_chance(sK1,X1,sK11)
| ~ reorganization(sK1,sK10,sK11)
| greater(X1,X0)
| X0 = X1 )
| ~ spl13_1
| ~ spl13_2
| ~ spl13_75 ),
inference(forward_subsumption_resolution,[],[f653,f614]) ).
fof(f671,plain,
( ! [X0,X1] :
( ~ survival_chance(sK2,X0,sK11)
| ~ survival_chance(sK1,X1,sK11)
| greater(X1,X0)
| X0 = X1 )
| ~ spl13_1
| ~ spl13_2
| ~ spl13_75 ),
inference(forward_subsumption_resolution,[],[f660,f52]) ).
fof(f696,plain,
( ! [X2,X0,X1] :
( ~ organization(sK1,X2)
| greater(X0,X1)
| ~ reorganization_free(sK1,sK11,X2)
| ~ survival_chance(sK1,X1,sK11)
| ~ survival_chance(sK1,X0,X2)
| ~ greater(X2,sK11) )
| ~ spl13_1 ),
inference(resolution,[],[f614,f39]) ).
fof(f698,plain,
( survival_chance(sK1,sK0(sK1,sK11),sK11)
| ~ spl13_1 ),
inference(resolution,[],[f614,f36]) ).
fof(f893,plain,
( ! [X0] :
( ~ survival_chance(sK1,X0,sK11)
| greater(X0,sK0(sK2,sK11))
| sK0(sK2,sK11) = X0 )
| ~ spl13_1
| ~ spl13_2
| ~ spl13_75 ),
inference(resolution,[],[f671,f659]) ).
fof(f918,plain,
( ! [X0,X1] :
( greater(X0,X1)
| ~ reorganization_free(sK1,sK11,sK12)
| ~ survival_chance(sK1,X1,sK11)
| ~ survival_chance(sK1,X0,sK12)
| ~ greater(sK12,sK11) )
| ~ spl13_1 ),
inference(resolution,[],[f696,f58]) ).
fof(f921,plain,
( ! [X0,X1] :
( greater(X0,X1)
| ~ survival_chance(sK1,X1,sK11)
| ~ survival_chance(sK1,X0,sK12)
| ~ greater(sK12,sK11) )
| ~ spl13_1 ),
inference(forward_subsumption_resolution,[],[f918,f48]) ).
fof(f922,plain,
( ! [X0,X1] :
( ~ survival_chance(sK1,X1,sK11)
| greater(X0,X1)
| ~ survival_chance(sK1,X0,sK12) )
| ~ spl13_1 ),
inference(forward_subsumption_resolution,[],[f921,f109]) ).
fof(f923,plain,
( ! [X2,X3,X0,X1] :
( greater(X0,X1)
| ~ reorganization(sK2,X2,X3)
| ~ survival_chance(sK2,X0,sK11)
| ~ survival_chance(sK2,X1,sK12)
| greater(X2,sK11)
| ~ greater(sK12,sK11)
| greater(sK12,X3) )
| ~ spl13_2 ),
inference(resolution,[],[f656,f57]) ).
fof(f926,plain,
( ! [X2,X3,X0,X1] :
( greater(X0,X1)
| ~ reorganization(sK2,X2,X3)
| ~ survival_chance(sK2,X0,sK11)
| ~ survival_chance(sK2,X1,sK12)
| greater(X2,sK11)
| greater(sK12,X3) )
| ~ spl13_1
| ~ spl13_2 ),
inference(forward_subsumption_resolution,[],[f923,f109]) ).
fof(f928,definition,
( spl13_119
<=> ! [X2,X3] :
( ~ reorganization(sK2,X2,X3)
| greater(sK12,X3)
| greater(X2,sK11) ) ),
introduced(definition,[new_symbols(definition,[spl13_119])],[avatar_definition]) ).
fof(f929,plain,
( ! [X2,X3] :
( ~ reorganization(sK2,X2,X3)
| greater(sK12,X3)
| greater(X2,sK11) )
| ~ spl13_119 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f931,definition,
( spl13_120
<=> ! [X0,X1] :
( greater(X0,X1)
| ~ survival_chance(sK2,X1,sK12)
| ~ survival_chance(sK2,X0,sK11) ) ),
introduced(definition,[new_symbols(definition,[spl13_120])],[avatar_definition]) ).
fof(f932,plain,
( ! [X0,X1] :
( ~ survival_chance(sK2,X1,sK12)
| greater(X0,X1)
| ~ survival_chance(sK2,X0,sK11) )
| ~ spl13_120 ),
inference(avatar_component_clause,[],[f931]) ).
fof(f933,plain,
( spl13_119
| spl13_120
| ~ spl13_1
| ~ spl13_2 ),
inference(avatar_split_clause,[],[f926,f112,f108,f931,f928]) ).
fof(f1062,plain,
( greater(sK12,sK12)
| greater(sK10,sK11)
| ~ spl13_119 ),
inference(resolution,[],[f929,f51]) ).
fof(f1063,plain,
( greater(sK10,sK11)
| spl13_3
| ~ spl13_119 ),
inference(forward_subsumption_resolution,[],[f1062,f121]) ).
fof(f1064,plain,
( $false
| spl13_3
| ~ spl13_119 ),
inference(forward_subsumption_resolution,[],[f1063,f71]) ).
fof(f1065,plain,
( spl13_3
| ~ spl13_119 ),
inference(avatar_contradiction_clause,[],[f1064]) ).
fof(f1068,plain,
( ! [X0] :
( ~ survival_chance(sK1,X0,sK12)
| greater(X0,sK0(sK1,sK11)) )
| ~ spl13_1 ),
inference(resolution,[],[f922,f698]) ).
fof(f1069,plain,
( ! [X0] :
( ~ survival_chance(sK2,X0,sK11)
| greater(X0,sK7) )
| ~ spl13_120 ),
inference(resolution,[],[f932,f46]) ).
fof(f1071,plain,
( greater(sK0(sK2,sK11),sK7)
| ~ spl13_2
| ~ spl13_120 ),
inference(resolution,[],[f1069,f659]) ).
fof(f1235,plain,
( greater(sK0(sK1,sK11),sK0(sK2,sK11))
| sK0(sK2,sK11) = sK0(sK1,sK11)
| ~ spl13_1
| ~ spl13_2
| ~ spl13_75 ),
inference(resolution,[],[f893,f698]) ).
fof(f1237,definition,
( spl13_161
<=> sK0(sK2,sK11) = sK0(sK1,sK11) ),
introduced(definition,[new_symbols(definition,[spl13_161])],[avatar_definition]) ).
fof(f1239,plain,
( sK0(sK2,sK11) = sK0(sK1,sK11)
| ~ spl13_161 ),
inference(avatar_component_clause,[],[f1237]) ).
fof(f1241,definition,
( spl13_162
<=> greater(sK0(sK1,sK11),sK0(sK2,sK11)) ),
introduced(definition,[new_symbols(definition,[spl13_162])],[avatar_definition]) ).
fof(f1243,plain,
( greater(sK0(sK1,sK11),sK0(sK2,sK11))
| ~ spl13_162 ),
inference(avatar_component_clause,[],[f1241]) ).
fof(f1244,plain,
( spl13_161
| spl13_162
| ~ spl13_1
| ~ spl13_2
| ~ spl13_75 ),
inference(avatar_split_clause,[],[f1235,f529,f112,f108,f1241,f1237]) ).
fof(f1254,plain,
( greater(sK6,sK0(sK1,sK11))
| ~ spl13_1 ),
inference(resolution,[],[f1068,f47]) ).
fof(f1270,plain,
( greater(sK0(sK1,sK11),sK7)
| ~ spl13_2
| ~ spl13_120
| ~ spl13_161 ),
inference(superposition,[],[f1071,f1239]) ).
fof(f1298,plain,
( ! [X0] :
( ~ greater(sK0(sK1,sK11),X0)
| greater(sK6,X0) )
| ~ spl13_1 ),
inference(resolution,[],[f1254,f35]) ).
fof(f1429,plain,
( greater(sK6,sK7)
| ~ spl13_1
| ~ spl13_2
| ~ spl13_120
| ~ spl13_161 ),
inference(resolution,[],[f1298,f1270]) ).
fof(f1431,plain,
( $false
| ~ spl13_1
| ~ spl13_2
| ~ spl13_120
| ~ spl13_161 ),
inference(forward_subsumption_resolution,[],[f1429,f61]) ).
fof(f1432,plain,
( ~ spl13_1
| ~ spl13_2
| ~ spl13_120
| ~ spl13_161 ),
inference(avatar_contradiction_clause,[],[f1431]) ).
fof(f1443,plain,
( ! [X0] :
( ~ greater(sK0(sK2,sK11),X0)
| greater(sK0(sK1,sK11),X0) )
| ~ spl13_162 ),
inference(resolution,[],[f1243,f35]) ).
fof(f1501,plain,
( greater(sK0(sK1,sK11),sK7)
| ~ spl13_2
| ~ spl13_120
| ~ spl13_162 ),
inference(resolution,[],[f1443,f1071]) ).
fof(f1503,plain,
( greater(sK6,sK7)
| ~ spl13_1
| ~ spl13_2
| ~ spl13_120
| ~ spl13_162 ),
inference(resolution,[],[f1501,f1298]) ).
fof(f1518,plain,
( $false
| ~ spl13_1
| ~ spl13_2
| ~ spl13_120
| ~ spl13_162 ),
inference(forward_subsumption_resolution,[],[f1503,f61]) ).
fof(f1519,plain,
( ~ spl13_1
| ~ spl13_2
| ~ spl13_120
| ~ spl13_162 ),
inference(avatar_contradiction_clause,[],[f1518]) ).
fof(f1525,plain,
( ~ greater(sK12,sK12)
| ~ spl13_3 ),
inference(resolution,[],[f120,f34]) ).
fof(f1546,plain,
( $false
| ~ spl13_3 ),
inference(forward_subsumption_resolution,[],[f1525,f120]) ).
fof(f1547,plain,
~ spl13_3,
inference(avatar_contradiction_clause,[],[f1546]) ).
cnf(s1,plain,
( ~ spl13_1
| spl13_2 ),
inference(sat_conversion,[],[f115]) ).
cnf(s22,plain,
( spl13_40
| spl13_41
| spl13_51
| spl13_52 ),
inference(sat_conversion,[],[f337]) ).
cnf(s23,plain,
~ spl13_40,
inference(sat_conversion,[],[f346]) ).
cnf(s24,plain,
~ spl13_41,
inference(sat_conversion,[],[f352]) ).
cnf(s47,plain,
~ spl13_51,
inference(sat_conversion,[],[f521]) ).
cnf(s48,plain,
( spl13_40
| spl13_41
| spl13_51
| spl13_73
| spl13_74
| spl13_75 ),
inference(sat_conversion,[],[f531]) ).
cnf(s49,plain,
~ spl13_73,
inference(sat_conversion,[],[f533]) ).
cnf(s50,plain,
~ spl13_74,
inference(sat_conversion,[],[f537]) ).
cnf(s60,plain,
( spl13_1
| ~ spl13_52 ),
inference(sat_conversion,[],[f613]) ).
cnf(s95,plain,
( ~ spl13_1
| ~ spl13_2
| spl13_119
| spl13_120 ),
inference(sat_conversion,[],[f933]) ).
cnf(s104,plain,
( spl13_3
| ~ spl13_119 ),
inference(sat_conversion,[],[f1065]) ).
cnf(s136,plain,
( ~ spl13_1
| ~ spl13_2
| ~ spl13_75
| spl13_161
| spl13_162 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s153,plain,
( ~ spl13_1
| ~ spl13_2
| ~ spl13_120
| ~ spl13_161 ),
inference(sat_conversion,[],[f1432]) ).
cnf(s163,plain,
( ~ spl13_1
| ~ spl13_2
| ~ spl13_120
| ~ spl13_162 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s167,plain,
~ spl13_3,
inference(sat_conversion,[],[f1547]) ).
cnf(s168,plain,
~ spl13_119,
inference(rat,[],[s104,s167]) ).
cnf(s169,plain,
( ~ spl13_1
| ~ spl13_2
| spl13_120 ),
inference(rat,[],[s95,s168]) ).
cnf(s170,plain,
( spl13_40
| spl13_41
| spl13_51
| spl13_75 ),
inference(rat,[],[s48,s50,s49]) ).
cnf(s173,plain,
spl13_75,
inference(rat,[],[s170,s24,s47,s23]) ).
cnf(s174,plain,
spl13_52,
inference(rat,[],[s22,s47,s24,s23]) ).
cnf(s175,plain,
spl13_1,
inference(rat,[],[s60,s174]) ).
cnf(s181,plain,
spl13_2,
inference(rat,[],[s1,s175]) ).
cnf(s182,plain,
spl13_120,
inference(rat,[],[s169,s175,s181]) ).
cnf(s184,plain,
~ spl13_162,
inference(rat,[],[s163,s181,s175,s182]) ).
cnf(s185,plain,
~ spl13_161,
inference(rat,[],[s153,s181,s175,s182]) ).
cnf(s186,plain,
$false,
inference(rat,[],[s136,s181,s175,s173,s184,s185]) ).
fof(f1548,plain,
$false,
inference(avatar_sat_refutation,[],[s186]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n010.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 17:16:02 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 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.37/0.47 % (1181057)Will run a generic schedule for satisfiability detection.
% 0.37/0.47 % (1181066)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=39683514:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.37/0.47 % (1181062)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2799178293_2999 on theBenchmark for (2999ds/0Mi)
% 0.37/0.47 % (1181064)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2944586862:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.37/0.47 % (1181065)dis+10_1_sil=32000:sp=arity:random_seed=3755702962:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.37/0.47 % (1181068)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2919814787:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.37/0.47 % (1181067)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3597236221:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.37/0.47 % (1181063)% WARNING: option uhcvi not known.
% 0.37/0.47 % TRYING [1]
% 0.37/0.47 % TRYING [2]
% 0.37/0.47 % (1181063)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2719260606:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.37/0.47 % TRYING [3]
% 0.37/0.47 % TRYING [4]
% 0.37/0.47 % (1181066)Instruction limit reached!
% 0.37/0.47 % (1181066)------------------------------
% 0.37/0.47 % (1181066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.37/0.47 % (1181066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.37/0.47 % (1181066)CaDiCaL version: 2.1.3
% 0.37/0.47 % (1181066)Termination reason: Instruction limit
% 0.37/0.47 % (1181066)Termination phase: Saturation
% 0.37/0.47 % (1181066)Time elapsed: 0.029 s
% 0.37/0.47 % (1181066)Peak memory usage: 12 MB
% 0.37/0.47 % (1181066)Instructions burned: 116 (million)
% 0.37/0.47 % (1181065) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1181057-1181065"...
% 0.37/0.47 % (1181067) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1181057-1181067"...
% 0.37/0.47 % (1181067)...printing done.
% 0.37/0.47 % (1181065)...printing done.
% 0.37/0.47 % (1181076)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3834716239:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.37/0.47 % (1181067)Refutation found. Thanks to Tanya!
% 0.37/0.47 % SZS status Theorem for theBenchmark
% 0.37/0.47 % SZS output start Proof for theBenchmark
% See solution above
% 0.37/0.47 % (1181067)------------------------------
% 0.37/0.47 % (1181067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.37/0.47 % (1181067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.37/0.47 % (1181067)CaDiCaL version: 2.1.3
% 0.37/0.47 % (1181067)Termination reason: Refutation
% 0.37/0.47 % (1181067)Time elapsed: 0.029 s
% 0.37/0.47 % (1181067)Peak memory usage: 13 MB
% 0.37/0.47 % (1181067)Instructions burned: 43 (million)
% 0.37/0.47 % (1181057)Success in time 0.066 s
% 0.37/0.47 % Vampire exiting
%------------------------------------------------------------------------------