%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : MGT010+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n002.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 : Theorem 0.57s 0.89s
% Output : Refutation 0.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 18
% Syntax : Number of clauses : 50 ( 20 unt; 0 nHn; 50 RR)
% Number of literals : 201 ( 0 equ; 154 neg)
% Maximal clause size : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 21 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
organization(skc21,skc20),
file('MGT010+1.p',unknown),
[] ).
cnf(2,axiom,
organization(skc19,skc18),
file('MGT010+1.p',unknown),
[] ).
cnf(3,axiom,
greater(skc12,skc11),
file('MGT010+1.p',unknown),
[] ).
cnf(4,axiom,
size(skc19,skc12,skc18),
file('MGT010+1.p',unknown),
[] ).
cnf(5,axiom,
accountability(skc19,skc13,skc18),
file('MGT010+1.p',unknown),
[] ).
cnf(6,axiom,
reliability(skc19,skc15,skc18),
file('MGT010+1.p',unknown),
[] ).
cnf(7,axiom,
class(skc19,skc17,skc18),
file('MGT010+1.p',unknown),
[] ).
cnf(8,axiom,
reorganization_free(skc19,skc18,skc18),
file('MGT010+1.p',unknown),
[] ).
cnf(9,axiom,
reorganization_free(skc21,skc20,skc20),
file('MGT010+1.p',unknown),
[] ).
cnf(10,axiom,
class(skc21,skc17,skc20),
file('MGT010+1.p',unknown),
[] ).
cnf(11,axiom,
reliability(skc21,skc16,skc20),
file('MGT010+1.p',unknown),
[] ).
cnf(12,axiom,
accountability(skc21,skc14,skc20),
file('MGT010+1.p',unknown),
[] ).
cnf(13,axiom,
size(skc21,skc11,skc20),
file('MGT010+1.p',unknown),
[] ).
cnf(14,axiom,
( ~ greater(skc13,skc14)
| ~ greater(skc15,skc16) ),
file('MGT010+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ organization(u,v)
| reproducibility(u,skf1(v,u),v) ),
file('MGT010+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ organization(u,v)
| ~ organization(w,x)
| ~ greater(y,z)
| ~ reliability(u,x1,v)
| ~ accountability(u,x2,v)
| ~ reproducibility(u,y,v)
| ~ reproducibility(w,z,x)
| ~ accountability(w,x3,x)
| ~ reliability(w,x4,x)
| greater(x2,x3) ),
file('MGT010+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ organization(u,v)
| ~ organization(w,x)
| ~ greater(y,z)
| ~ reliability(u,x1,v)
| ~ accountability(u,x2,v)
| ~ reproducibility(u,y,v)
| ~ reproducibility(w,z,x)
| ~ accountability(w,x3,x)
| ~ reliability(w,x4,x)
| greater(x1,x4) ),
file('MGT010+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ greater(u,v)
| ~ organization(w,x)
| ~ organization(y,z)
| ~ size(w,v,x)
| ~ reproducibility(w,x1,x)
| ~ class(w,x2,x)
| ~ reorganization_free(w,x,x)
| ~ reorganization_free(y,z,z)
| ~ class(y,x2,z)
| ~ reproducibility(y,x3,z)
| ~ size(y,u,z)
| greater(x3,x1) ),
file('MGT010+1.p',unknown),
[] ).
cnf(25,plain,
reproducibility(skc19,skf1(skc18,skc19),skc18),
inference(res,[status(thm),theory(equality)],[2,15]),
[iquote('0:Res:2.0,15.0')] ).
cnf(26,plain,
( ~ size(skc19,u,skc18)
| ~ reproducibility(skc19,v,skc18)
| ~ class(skc19,w,skc18)
| ~ reorganization_free(skc19,skc18,skc18)
| ~ organization(x,y)
| ~ reorganization_free(x,y,y)
| ~ class(x,w,y)
| ~ reproducibility(x,z,y)
| ~ size(x,x1,y)
| ~ greater(u,x1)
| greater(v,z) ),
inference(res,[status(thm),theory(equality)],[2,19]),
[iquote('0:Res:2.0,19.4')] ).
cnf(34,plain,
reproducibility(skc21,skf1(skc20,skc21),skc20),
inference(res,[status(thm),theory(equality)],[1,15]),
[iquote('0:Res:1.0,15.0')] ).
cnf(36,plain,
( ~ organization(u,v)
| ~ greater(w,x)
| ~ reliability(u,y,v)
| ~ accountability(u,z,v)
| ~ reproducibility(u,w,v)
| ~ reproducibility(skc21,x,skc20)
| ~ accountability(skc21,x1,skc20)
| ~ reliability(skc21,x2,skc20)
| greater(y,x2) ),
inference(res,[status(thm),theory(equality)],[1,17]),
[iquote('0:Res:1.0,17.1')] ).
cnf(37,plain,
( ~ organization(u,v)
| ~ greater(w,x)
| ~ reliability(u,y,v)
| ~ accountability(u,z,v)
| ~ reproducibility(u,w,v)
| ~ reproducibility(skc21,x,skc20)
| ~ accountability(skc21,x1,skc20)
| ~ reliability(skc21,x2,skc20)
| greater(z,x1) ),
inference(res,[status(thm),theory(equality)],[1,16]),
[iquote('0:Res:1.0,16.1')] ).
cnf(46,plain,
( ~ greater(u,v)
| ~ organization(w,x)
| ~ size(w,v,x)
| ~ reproducibility(w,y,x)
| ~ class(w,z,x)
| ~ reorganization_free(w,x,x)
| ~ class(skc19,z,skc18)
| ~ reproducibility(skc19,x1,skc18)
| ~ size(skc19,u,skc18)
| greater(x1,y) ),
inference(mrr,[status(thm)],[26,8]),
[iquote('0:MRR:26.3,8.0')] ).
cnf(114,plain,
( ~ organization(skc19,skc18)
| ~ greater(u,v)
| ~ accountability(skc19,w,skc18)
| ~ reproducibility(skc19,u,skc18)
| ~ reproducibility(skc21,v,skc20)
| ~ accountability(skc21,x,skc20)
| ~ reliability(skc21,y,skc20)
| greater(skc15,y) ),
inference(res,[status(thm),theory(equality)],[6,36]),
[iquote('0:Res:6.0,36.2')] ).
cnf(115,plain,
( ~ greater(u,v)
| ~ accountability(skc19,w,skc18)
| ~ reproducibility(skc19,u,skc18)
| ~ reproducibility(skc21,v,skc20)
| ~ accountability(skc21,x,skc20)
| ~ reliability(skc21,y,skc20)
| greater(skc15,y) ),
inference(mrr,[status(thm)],[114,2]),
[iquote('0:MRR:114.0,2.0')] ).
cnf(117,plain,
( ~ greater(u,v)
| ~ reproducibility(skc19,u,skc18)
| ~ reproducibility(skc21,v,skc20)
| ~ accountability(skc21,w,skc20)
| ~ reliability(skc21,x,skc20)
| greater(skc15,x) ),
inference(res,[status(thm),theory(equality)],[5,115]),
[iquote('0:Res:5.0,115.1')] ).
cnf(118,plain,
( ~ greater(skf1(skc18,skc19),u)
| ~ reproducibility(skc21,u,skc20)
| ~ accountability(skc21,v,skc20)
| ~ reliability(skc21,w,skc20)
| greater(skc15,w) ),
inference(res,[status(thm),theory(equality)],[25,117]),
[iquote('0:Res:25.0,117.1')] ).
cnf(122,plain,
( ~ organization(skc19,skc18)
| ~ greater(u,v)
| ~ accountability(skc19,w,skc18)
| ~ reproducibility(skc19,u,skc18)
| ~ reproducibility(skc21,v,skc20)
| ~ accountability(skc21,x,skc20)
| ~ reliability(skc21,y,skc20)
| greater(w,x) ),
inference(res,[status(thm),theory(equality)],[6,37]),
[iquote('0:Res:6.0,37.2')] ).
cnf(123,plain,
( ~ greater(u,v)
| ~ accountability(skc19,w,skc18)
| ~ reproducibility(skc19,u,skc18)
| ~ reproducibility(skc21,v,skc20)
| ~ accountability(skc21,x,skc20)
| ~ reliability(skc21,y,skc20)
| greater(w,x) ),
inference(mrr,[status(thm)],[122,2]),
[iquote('0:MRR:122.0,2.0')] ).
cnf(124,plain,
( ~ greater(u,v)
| ~ reproducibility(skc19,u,skc18)
| ~ reproducibility(skc21,v,skc20)
| ~ accountability(skc21,w,skc20)
| ~ reliability(skc21,x,skc20)
| greater(skc13,w) ),
inference(res,[status(thm),theory(equality)],[5,123]),
[iquote('0:Res:5.0,123.1')] ).
cnf(125,plain,
( ~ greater(skf1(skc18,skc19),u)
| ~ reproducibility(skc21,u,skc20)
| ~ accountability(skc21,v,skc20)
| ~ reliability(skc21,w,skc20)
| greater(skc13,v) ),
inference(res,[status(thm),theory(equality)],[25,124]),
[iquote('0:Res:25.0,124.1')] ).
cnf(290,plain,
( ~ greater(u,skc11)
| ~ organization(skc21,skc20)
| ~ reproducibility(skc21,v,skc20)
| ~ class(skc21,w,skc20)
| ~ reorganization_free(skc21,skc20,skc20)
| ~ class(skc19,w,skc18)
| ~ reproducibility(skc19,x,skc18)
| ~ size(skc19,u,skc18)
| greater(x,v) ),
inference(res,[status(thm),theory(equality)],[13,46]),
[iquote('0:Res:13.0,46.2')] ).
cnf(294,plain,
( ~ greater(u,skc11)
| ~ reproducibility(skc21,v,skc20)
| ~ class(skc21,w,skc20)
| ~ class(skc19,w,skc18)
| ~ reproducibility(skc19,x,skc18)
| ~ size(skc19,u,skc18)
| greater(x,v) ),
inference(mrr,[status(thm)],[290,1,9]),
[iquote('0:MRR:290.1,290.4,1.0,9.0')] ).
cnf(318,plain,
( ~ greater(u,skc11)
| ~ class(skc21,v,skc20)
| ~ class(skc19,v,skc18)
| ~ reproducibility(skc19,w,skc18)
| ~ size(skc19,u,skc18)
| greater(w,skf1(skc20,skc21)) ),
inference(res,[status(thm),theory(equality)],[34,294]),
[iquote('0:Res:34.0,294.1')] ).
cnf(378,plain,
( ~ greater(u,skc11)
| ~ class(skc19,skc17,skc18)
| ~ reproducibility(skc19,v,skc18)
| ~ size(skc19,u,skc18)
| greater(v,skf1(skc20,skc21)) ),
inference(res,[status(thm),theory(equality)],[10,318]),
[iquote('0:Res:10.0,318.1')] ).
cnf(379,plain,
( ~ greater(u,skc11)
| ~ reproducibility(skc19,v,skc18)
| ~ size(skc19,u,skc18)
| greater(v,skf1(skc20,skc21)) ),
inference(mrr,[status(thm)],[378,7]),
[iquote('0:MRR:378.1,7.0')] ).
cnf(380,plain,
( ~ greater(u,skc11)
| ~ size(skc19,u,skc18)
| greater(skf1(skc18,skc19),skf1(skc20,skc21)) ),
inference(res,[status(thm),theory(equality)],[25,379]),
[iquote('0:Res:25.0,379.1')] ).
cnf(382,plain,
( ~ greater(skc12,skc11)
| greater(skf1(skc18,skc19),skf1(skc20,skc21)) ),
inference(res,[status(thm),theory(equality)],[4,380]),
[iquote('0:Res:4.0,380.1')] ).
cnf(383,plain,
greater(skf1(skc18,skc19),skf1(skc20,skc21)),
inference(mrr,[status(thm)],[382,3]),
[iquote('0:MRR:382.0,3.0')] ).
cnf(384,plain,
( ~ reproducibility(skc21,skf1(skc20,skc21),skc20)
| ~ accountability(skc21,u,skc20)
| ~ reliability(skc21,v,skc20)
| greater(skc13,u) ),
inference(res,[status(thm),theory(equality)],[383,125]),
[iquote('0:Res:383.0,125.0')] ).
cnf(385,plain,
( ~ reproducibility(skc21,skf1(skc20,skc21),skc20)
| ~ accountability(skc21,u,skc20)
| ~ reliability(skc21,v,skc20)
| greater(skc15,v) ),
inference(res,[status(thm),theory(equality)],[383,118]),
[iquote('0:Res:383.0,118.0')] ).
cnf(391,plain,
( ~ accountability(skc21,u,skc20)
| ~ reliability(skc21,v,skc20)
| greater(skc15,v) ),
inference(mrr,[status(thm)],[385,34]),
[iquote('0:MRR:385.0,34.0')] ).
cnf(394,plain,
( ~ accountability(skc21,u,skc20)
| ~ reliability(skc21,v,skc20)
| greater(skc13,u) ),
inference(mrr,[status(thm)],[384,34]),
[iquote('0:MRR:384.0,34.0')] ).
cnf(400,plain,
( ~ reliability(skc21,u,skc20)
| greater(skc15,u) ),
inference(res,[status(thm),theory(equality)],[12,391]),
[iquote('0:Res:12.0,391.0')] ).
cnf(401,plain,
greater(skc15,skc16),
inference(res,[status(thm),theory(equality)],[11,400]),
[iquote('0:Res:11.0,400.0')] ).
cnf(402,plain,
~ greater(skc13,skc14),
inference(mrr,[status(thm)],[14,401]),
[iquote('0:MRR:14.1,401.0')] ).
cnf(405,plain,
( ~ reliability(skc21,u,skc20)
| greater(skc13,skc14) ),
inference(res,[status(thm),theory(equality)],[12,394]),
[iquote('0:Res:12.0,394.0')] ).
cnf(406,plain,
~ reliability(skc21,u,skc20),
inference(mrr,[status(thm)],[405,402]),
[iquote('0:MRR:405.1,402.0')] ).
cnf(407,plain,
$false,
inference(unc,[status(thm)],[406,11]),
[iquote('0:UnC:406.0,11.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT010+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.06 % Command : run_spass %d %s
% 0.16/0.41 % Computer : n002.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 7 11:49:52 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.57/0.89
% 0.57/0.89 SPASS V 3.9
% 0.57/0.89 SPASS beiseite: Proof found.
% 0.57/0.89 % SZS status Theorem
% 0.57/0.89 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/0.89 SPASS derived 283 clauses, backtracked 0 clauses, performed 0 splits and kept 240 clauses.
% 0.57/0.89 SPASS allocated 85573 KBytes.
% 0.57/0.89 SPASS spent 0:00:00.44 on the problem.
% 0.57/0.89 0:00:00.09 for the input.
% 0.57/0.89 0:00:00.09 for the FLOTTER CNF translation.
% 0.57/0.89 0:00:00.02 for inferences.
% 0.57/0.89 0:00:00.00 for the backtracking.
% 0.57/0.89 0:00:00.16 for the reduction.
% 0.57/0.89
% 0.57/0.89
% 0.57/0.89 Here is a proof with depth 9, length 50 :
% 0.57/0.89 % SZS output start Refutation
% See solution above
% 0.57/0.89 Formulae used in the proof : t10_FOL mp3 a2_FOL t9_FOL
% 0.57/0.89
%------------------------------------------------------------------------------