%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : MGT008-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.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 8 06:19:45 AM UTC 2026
% Result : Unsatisfiable 0.13s 0.70s
% Output : Refutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 15
% Syntax : Number of clauses : 32 ( 15 unt; 0 nHn; 32 RR)
% Number of literals : 110 ( 0 equ; 82 neg)
% Maximal clause size : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 18 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ organization(u,v)
| inertia(u,sk1(v,u),v) ),
file('MGT008-1.p',unknown),
[] ).
cnf(2,axiom,
( ~ greater(u,v)
| ~ organization(w,x)
| ~ organization(y,z)
| ~ inertia(w,x1,x)
| ~ inertia(y,x2,z)
| ~ size(w,u,x)
| ~ size(y,v,z)
| ~ class(w,x3,x)
| ~ class(y,x3,z)
| greater(x1,x2) ),
file('MGT008-1.p',unknown),
[] ).
cnf(3,axiom,
( ~ greater(u,v)
| ~ organization(w,x)
| ~ organization(y,z)
| ~ survival_chance(w,x1,x)
| ~ survival_chance(y,x2,z)
| ~ inertia(w,u,x)
| ~ inertia(y,v,z)
| ~ reorganization_free(w,x,x)
| ~ reorganization_free(y,z,z)
| greater(x1,x2) ),
file('MGT008-1.p',unknown),
[] ).
cnf(4,axiom,
organization(sk2,sk9),
file('MGT008-1.p',unknown),
[] ).
cnf(5,axiom,
organization(sk3,sk10),
file('MGT008-1.p',unknown),
[] ).
cnf(6,axiom,
reorganization_free(sk2,sk9,sk9),
file('MGT008-1.p',unknown),
[] ).
cnf(7,axiom,
reorganization_free(sk3,sk10,sk10),
file('MGT008-1.p',unknown),
[] ).
cnf(8,axiom,
class(sk2,sk4,sk9),
file('MGT008-1.p',unknown),
[] ).
cnf(9,axiom,
class(sk3,sk4,sk10),
file('MGT008-1.p',unknown),
[] ).
cnf(10,axiom,
survival_chance(sk2,sk5,sk9),
file('MGT008-1.p',unknown),
[] ).
cnf(11,axiom,
survival_chance(sk3,sk6,sk10),
file('MGT008-1.p',unknown),
[] ).
cnf(12,axiom,
size(sk2,sk7,sk9),
file('MGT008-1.p',unknown),
[] ).
cnf(13,axiom,
size(sk3,sk8,sk10),
file('MGT008-1.p',unknown),
[] ).
cnf(14,axiom,
greater(sk8,sk7),
file('MGT008-1.p',unknown),
[] ).
cnf(15,axiom,
~ greater(sk6,sk5),
file('MGT008-1.p',unknown),
[] ).
cnf(20,plain,
inertia(sk3,sk1(sk10,sk3),sk10),
inference(res,[status(thm),theory(equality)],[5,1]),
[iquote('0:Res:5.0,1.0')] ).
cnf(25,plain,
inertia(sk2,sk1(sk9,sk2),sk9),
inference(res,[status(thm),theory(equality)],[4,1]),
[iquote('0:Res:4.0,1.0')] ).
cnf(31,plain,
( ~ organization(u,v)
| ~ organization(sk3,sk10)
| ~ class(u,w,v)
| ~ class(sk3,w,sk10)
| ~ size(u,x,v)
| ~ inertia(u,y,v)
| ~ inertia(sk3,z,sk10)
| ~ greater(sk8,x)
| greater(z,y) ),
inference(res,[status(thm),theory(equality)],[13,2]),
[iquote('0:Res:13.0,2.5')] ).
cnf(32,plain,
( ~ organization(u,v)
| ~ greater(sk8,w)
| ~ inertia(u,x,v)
| ~ size(u,w,v)
| ~ class(u,y,v)
| ~ inertia(sk3,z,sk10)
| ~ class(sk3,y,sk10)
| greater(z,x) ),
inference(mrr,[status(thm)],[31,5]),
[iquote('0:MRR:31.1,5.0')] ).
cnf(38,plain,
( ~ organization(sk2,sk9)
| ~ greater(sk8,u)
| ~ size(sk2,u,sk9)
| ~ class(sk2,v,sk9)
| ~ inertia(sk3,w,sk10)
| ~ class(sk3,v,sk10)
| greater(w,sk1(sk9,sk2)) ),
inference(res,[status(thm),theory(equality)],[25,32]),
[iquote('0:Res:25.0,32.2')] ).
cnf(43,plain,
( ~ greater(sk8,u)
| ~ size(sk2,u,sk9)
| ~ class(sk2,v,sk9)
| ~ inertia(sk3,w,sk10)
| ~ class(sk3,v,sk10)
| greater(w,sk1(sk9,sk2)) ),
inference(mrr,[status(thm)],[38,4]),
[iquote('0:MRR:38.0,4.0')] ).
cnf(49,plain,
( ~ greater(u,v)
| ~ organization(sk3,sk10)
| ~ organization(w,x)
| ~ survival_chance(w,y,x)
| ~ inertia(sk3,u,sk10)
| ~ inertia(w,v,x)
| ~ reorganization_free(sk3,sk10,sk10)
| ~ reorganization_free(w,x,x)
| greater(sk6,y) ),
inference(res,[status(thm),theory(equality)],[11,3]),
[iquote('0:Res:11.0,3.3')] ).
cnf(52,plain,
( ~ greater(u,v)
| ~ organization(w,x)
| ~ survival_chance(w,y,x)
| ~ inertia(sk3,u,sk10)
| ~ inertia(w,v,x)
| ~ reorganization_free(w,x,x)
| greater(sk6,y) ),
inference(mrr,[status(thm)],[49,5,7]),
[iquote('0:MRR:49.1,49.6,5.0,7.0')] ).
cnf(53,plain,
( ~ greater(sk8,sk7)
| ~ class(sk2,u,sk9)
| ~ inertia(sk3,v,sk10)
| ~ class(sk3,u,sk10)
| greater(v,sk1(sk9,sk2)) ),
inference(res,[status(thm),theory(equality)],[12,43]),
[iquote('0:Res:12.0,43.1')] ).
cnf(54,plain,
( ~ class(sk2,u,sk9)
| ~ inertia(sk3,v,sk10)
| ~ class(sk3,u,sk10)
| greater(v,sk1(sk9,sk2)) ),
inference(mrr,[status(thm)],[53,14]),
[iquote('0:MRR:53.0,14.0')] ).
cnf(55,plain,
( ~ inertia(sk3,u,sk10)
| ~ class(sk3,sk4,sk10)
| greater(u,sk1(sk9,sk2)) ),
inference(res,[status(thm),theory(equality)],[8,54]),
[iquote('0:Res:8.0,54.0')] ).
cnf(56,plain,
( ~ inertia(sk3,u,sk10)
| greater(u,sk1(sk9,sk2)) ),
inference(mrr,[status(thm)],[55,9]),
[iquote('0:MRR:55.1,9.0')] ).
cnf(72,plain,
( ~ greater(u,v)
| ~ organization(sk2,sk9)
| ~ inertia(sk3,u,sk10)
| ~ inertia(sk2,v,sk9)
| ~ reorganization_free(sk2,sk9,sk9)
| greater(sk6,sk5) ),
inference(res,[status(thm),theory(equality)],[10,52]),
[iquote('0:Res:10.0,52.2')] ).
cnf(73,plain,
( ~ greater(u,v)
| ~ inertia(sk3,u,sk10)
| ~ inertia(sk2,v,sk9) ),
inference(mrr,[status(thm)],[72,4,6,15]),
[iquote('0:MRR:72.1,72.4,72.5,4.0,6.0,15.0')] ).
cnf(75,plain,
( ~ greater(sk1(sk10,sk3),u)
| ~ inertia(sk2,u,sk9) ),
inference(res,[status(thm),theory(equality)],[20,73]),
[iquote('0:Res:20.0,73.1')] ).
cnf(78,plain,
( ~ inertia(sk3,sk1(sk10,sk3),sk10)
| ~ inertia(sk2,sk1(sk9,sk2),sk9) ),
inference(res,[status(thm),theory(equality)],[56,75]),
[iquote('0:Res:56.1,75.0')] ).
cnf(79,plain,
$false,
inference(mrr,[status(thm)],[78,20,25]),
[iquote('0:MRR:78.0,78.1,20.0,25.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT008-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : run_spass %d %s
% 0.09/0.56 % Computer : n029.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Mon Sep 7 11:46:57 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.13/0.70
% 0.13/0.70 SPASS V 3.9
% 0.13/0.70 SPASS beiseite: Proof found.
% 0.13/0.70 % SZS status Theorem
% 0.13/0.70 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.70 SPASS derived 41 clauses, backtracked 0 clauses, performed 0 splits and kept 53 clauses.
% 0.13/0.70 SPASS allocated 63224 KBytes.
% 0.13/0.70 SPASS spent 0:00:00.12 on the problem.
% 0.13/0.70 0:00:00.06 for the input.
% 0.13/0.70 0:00:00.00 for the FLOTTER CNF translation.
% 0.13/0.70 0:00:00.00 for inferences.
% 0.13/0.70 0:00:00.00 for the backtracking.
% 0.13/0.70 0:00:00.01 for the reduction.
% 0.13/0.70
% 0.13/0.70
% 0.13/0.70 Here is a proof with depth 5, length 32 :
% 0.13/0.70 % SZS output start Refutation
% See solution above
% 0.13/0.70 Formulae used in the proof : mp5_1 a5_FOL_2 t1_FOL_3 t8_FOL_4 t8_FOL_5 t8_FOL_6 t8_FOL_7 t8_FOL_8 t8_FOL_9 t8_FOL_10 t8_FOL_11 t8_FOL_12 t8_FOL_13 t8_FOL_14 t8_FOL_15
% 0.13/0.70
%------------------------------------------------------------------------------