%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : MGT007-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% 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 8 06:19:45 AM UTC 2026
% Result : Unsatisfiable 0.32s 0.59s
% Output : Refutation 0.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 14
% Syntax : Number of clauses : 34 ( 14 unt; 6 nHn; 34 RR)
% Number of literals : 149 ( 0 equ; 114 neg)
% Maximal clause size : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ organization(u,v)
| reliability(u,sk1(v,u),v) ),
file('MGT007-1.p',unknown),
[] ).
cnf(2,axiom,
( ~ organization(u,v)
| accountability(u,sk2(v,u),v) ),
file('MGT007-1.p',unknown),
[] ).
cnf(6,axiom,
( ~ greater(u,v)
| ~ greater(w,x)
| ~ organization(y,z)
| ~ organization(x1,x2)
| ~ reproducibility(y,x3,z)
| ~ reproducibility(x1,x4,x2)
| ~ accountability(y,u,z)
| ~ accountability(x1,v,x2)
| ~ reliability(y,w,z)
| ~ reliability(x1,x,x2)
| greater(x3,x4) ),
file('MGT007-1.p',unknown),
[] ).
cnf(7,axiom,
( ~ greater(u,v)
| ~ organization(w,u)
| ~ organization(w,v)
| ~ accountability(w,x,u)
| ~ accountability(w,y,v)
| ~ reliability(w,z,u)
| ~ reliability(w,x1,v)
| ~ reorganization(w,x2,x3)
| greater(x1,z)
| greater(u,x3)
| greater(x2,v) ),
file('MGT007-1.p',unknown),
[] ).
cnf(8,axiom,
( ~ greater(u,v)
| ~ organization(w,u)
| ~ organization(w,v)
| ~ accountability(w,x,u)
| ~ accountability(w,y,v)
| ~ reliability(w,z,u)
| ~ reliability(w,x1,v)
| ~ reorganization(w,x2,x3)
| greater(y,x)
| greater(u,x3)
| greater(x2,v) ),
file('MGT007-1.p',unknown),
[] ).
cnf(9,axiom,
organization(sk4,sk7),
file('MGT007-1.p',unknown),
[] ).
cnf(10,axiom,
organization(sk4,sk8),
file('MGT007-1.p',unknown),
[] ).
cnf(11,axiom,
reorganization(sk4,sk9,sk10),
file('MGT007-1.p',unknown),
[] ).
cnf(12,axiom,
reproducibility(sk4,sk5,sk7),
file('MGT007-1.p',unknown),
[] ).
cnf(13,axiom,
reproducibility(sk4,sk6,sk8),
file('MGT007-1.p',unknown),
[] ).
cnf(14,axiom,
~ greater(sk9,sk7),
file('MGT007-1.p',unknown),
[] ).
cnf(15,axiom,
greater(sk8,sk7),
file('MGT007-1.p',unknown),
[] ).
cnf(16,axiom,
~ greater(sk8,sk10),
file('MGT007-1.p',unknown),
[] ).
cnf(17,axiom,
~ greater(sk5,sk6),
file('MGT007-1.p',unknown),
[] ).
cnf(22,plain,
( ~ organization(u,sk8)
| ~ organization(u,sk7)
| ~ reorganization(u,v,w)
| ~ accountability(u,x,sk8)
| ~ accountability(u,y,sk7)
| ~ reliability(u,z,sk8)
| ~ reliability(u,x1,sk7)
| greater(y,x)
| greater(v,sk7)
| greater(sk8,w) ),
inference(res,[status(thm),theory(equality)],[15,8]),
[iquote('0:Res:15.0,8.7')] ).
cnf(23,plain,
( ~ organization(u,sk8)
| ~ organization(u,sk7)
| ~ reorganization(u,v,w)
| ~ accountability(u,x,sk8)
| ~ accountability(u,y,sk7)
| ~ reliability(u,z,sk8)
| ~ reliability(u,x1,sk7)
| greater(x1,z)
| greater(v,sk7)
| greater(sk8,w) ),
inference(res,[status(thm),theory(equality)],[15,7]),
[iquote('0:Res:15.0,7.7')] ).
cnf(29,plain,
reliability(sk4,sk1(sk8,sk4),sk8),
inference(res,[status(thm),theory(equality)],[10,1]),
[iquote('0:Res:10.0,1.0')] ).
cnf(30,plain,
accountability(sk4,sk2(sk8,sk4),sk8),
inference(res,[status(thm),theory(equality)],[10,2]),
[iquote('0:Res:10.0,2.0')] ).
cnf(113,plain,
( ~ greater(u,v)
| ~ greater(w,x)
| ~ organization(sk4,sk7)
| ~ organization(y,z)
| ~ reproducibility(y,x1,z)
| ~ accountability(sk4,u,sk7)
| ~ accountability(y,v,z)
| ~ reliability(sk4,w,sk7)
| ~ reliability(y,x,z)
| greater(sk5,x1) ),
inference(res,[status(thm),theory(equality)],[12,6]),
[iquote('0:Res:12.0,6.4')] ).
cnf(115,plain,
( ~ greater(u,v)
| ~ greater(w,x)
| ~ organization(y,z)
| ~ reproducibility(y,x1,z)
| ~ accountability(sk4,u,sk7)
| ~ accountability(y,v,z)
| ~ reliability(sk4,w,sk7)
| ~ reliability(y,x,z)
| greater(sk5,x1) ),
inference(mrr,[status(thm)],[113,9]),
[iquote('0:MRR:113.2,9.0')] ).
cnf(153,plain,
( ~ greater(u,v)
| ~ greater(w,x)
| ~ organization(sk4,sk8)
| ~ accountability(sk4,u,sk7)
| ~ accountability(sk4,v,sk8)
| ~ reliability(sk4,w,sk7)
| ~ reliability(sk4,x,sk8)
| greater(sk5,sk6) ),
inference(res,[status(thm),theory(equality)],[13,115]),
[iquote('0:Res:13.0,115.3')] ).
cnf(158,plain,
( ~ greater(u,v)
| ~ greater(w,x)
| ~ accountability(sk4,u,sk7)
| ~ accountability(sk4,v,sk8)
| ~ reliability(sk4,w,sk7)
| ~ reliability(sk4,x,sk8) ),
inference(mrr,[status(thm)],[153,10,17]),
[iquote('0:MRR:153.2,153.7,10.0,17.0')] ).
cnf(304,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| ~ accountability(sk4,u,sk8)
| ~ accountability(sk4,v,sk7)
| ~ reliability(sk4,w,sk8)
| ~ reliability(sk4,x,sk7)
| greater(v,u)
| greater(sk9,sk7)
| greater(sk8,sk10) ),
inference(res,[status(thm),theory(equality)],[11,22]),
[iquote('0:Res:11.0,22.2')] ).
cnf(305,plain,
( ~ accountability(sk4,u,sk8)
| ~ accountability(sk4,v,sk7)
| ~ reliability(sk4,w,sk8)
| ~ reliability(sk4,x,sk7)
| greater(v,u) ),
inference(mrr,[status(thm)],[304,10,9,14,16]),
[iquote('0:MRR:304.0,304.1,304.7,304.8,10.0,9.0,14.0,16.0')] ).
cnf(306,plain,
( ~ greater(u,v)
| ~ accountability(sk4,w,sk7)
| ~ accountability(sk4,x,sk8)
| ~ reliability(sk4,u,sk7)
| ~ reliability(sk4,v,sk8) ),
inference(mrr,[status(thm)],[158,305]),
[iquote('0:MRR:158.0,305.4')] ).
cnf(317,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| ~ accountability(sk4,u,sk8)
| ~ accountability(sk4,v,sk7)
| ~ reliability(sk4,w,sk8)
| ~ reliability(sk4,x,sk7)
| greater(x,w)
| greater(sk9,sk7)
| greater(sk8,sk10) ),
inference(res,[status(thm),theory(equality)],[11,23]),
[iquote('0:Res:11.0,23.2')] ).
cnf(318,plain,
( ~ accountability(sk4,u,sk8)
| ~ accountability(sk4,v,sk7)
| ~ reliability(sk4,w,sk8)
| ~ reliability(sk4,x,sk7)
| greater(x,w) ),
inference(mrr,[status(thm)],[317,10,9,14,16]),
[iquote('0:MRR:317.0,317.1,317.7,317.8,10.0,9.0,14.0,16.0')] ).
cnf(319,plain,
( ~ accountability(sk4,u,sk8)
| ~ accountability(sk4,v,sk7)
| ~ reliability(sk4,w,sk8)
| ~ reliability(sk4,x,sk7) ),
inference(mrr,[status(thm)],[318,306]),
[iquote('0:MRR:318.4,306.0')] ).
cnf(333,plain,
( ~ accountability(sk4,u,sk7)
| ~ reliability(sk4,v,sk8)
| ~ reliability(sk4,w,sk7) ),
inference(res,[status(thm),theory(equality)],[30,319]),
[iquote('0:Res:30.0,319.0')] ).
cnf(337,plain,
( ~ organization(sk4,sk7)
| ~ reliability(sk4,u,sk8)
| ~ reliability(sk4,v,sk7) ),
inference(res,[status(thm),theory(equality)],[2,333]),
[iquote('0:Res:2.1,333.0')] ).
cnf(338,plain,
( ~ reliability(sk4,u,sk8)
| ~ reliability(sk4,v,sk7) ),
inference(mrr,[status(thm)],[337,9]),
[iquote('0:MRR:337.0,9.0')] ).
cnf(339,plain,
~ reliability(sk4,u,sk7),
inference(res,[status(thm),theory(equality)],[29,338]),
[iquote('0:Res:29.0,338.0')] ).
cnf(341,plain,
~ organization(sk4,sk7),
inference(res,[status(thm),theory(equality)],[1,339]),
[iquote('0:Res:1.1,339.0')] ).
cnf(342,plain,
$false,
inference(mrr,[status(thm)],[341,9]),
[iquote('0:MRR:341.0,9.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT007-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.08/0.34 % Computer : n004.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 11:44:00 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.32/0.59
% 0.32/0.59 SPASS V 3.9
% 0.32/0.59 SPASS beiseite: Proof found.
% 0.32/0.59 % SZS status Theorem
% 0.32/0.59 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/0.59 SPASS derived 213 clauses, backtracked 0 clauses, performed 2 splits and kept 179 clauses.
% 0.32/0.59 SPASS allocated 63564 KBytes.
% 0.32/0.59 SPASS spent 0:00:00.22 on the problem.
% 0.32/0.59 0:00:00.06 for the input.
% 0.32/0.59 0:00:00.00 for the FLOTTER CNF translation.
% 0.32/0.59 0:00:00.01 for inferences.
% 0.32/0.59 0:00:00.00 for the backtracking.
% 0.32/0.59 0:00:00.09 for the reduction.
% 0.32/0.59
% 0.32/0.59
% 0.32/0.59 Here is a proof with depth 6, length 34 :
% 0.32/0.59 % SZS output start Refutation
% See solution above
% 0.32/0.59 Formulae used in the proof : mp1_1 mp2_2 a2_FOL_6 a6_FOL_7 a6_FOL_8 t7_FOL_9 t7_FOL_10 t7_FOL_11 t7_FOL_12 t7_FOL_13 t7_FOL_14 t7_FOL_15 t7_FOL_16 t7_FOL_17
% 0.32/0.59
%------------------------------------------------------------------------------