%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT001-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:18:36 AM UTC 2026
% Result : Unsatisfiable 0.24s 0.59s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 17
% Syntax : Number of clauses : 61 ( 21 unt; 0 nHn; 61 RR)
% Number of literals : 254 ( 0 equ; 194 neg)
% Maximal clause size : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 117 ( 22 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1_FOL_19,negated_conjecture,
~ greater(sk11,sk10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_19) ).
cnf(t1_FOL_10,negated_conjecture,
organization(sk4,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_10) ).
cnf(t1_FOL_11,negated_conjecture,
organization(sk5,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_11) ).
cnf(mp1_1,axiom,
( ~ organization(X3,X2)
| reliability(X3,sk1(X2,X3),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp1_1) ).
cnf(c1,plain,
reliability(sk4,sk1(sk6,sk4),sk6),
inference(resolution,[status(thm)],[mp1_1,t1_FOL_10]) ).
cnf(c0,plain,
reliability(sk5,sk1(sk7,sk5),sk7),
inference(resolution,[status(thm)],[mp1_1,t1_FOL_11]) ).
cnf(mp2_2,axiom,
( ~ organization(X5,X4)
| accountability(X5,sk2(X4,X5),X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp2_2) ).
cnf(c3,plain,
accountability(sk4,sk2(sk6,sk4),sk6),
inference(resolution,[status(thm)],[mp2_2,t1_FOL_10]) ).
cnf(c2,plain,
accountability(sk5,sk2(sk7,sk5),sk7),
inference(resolution,[status(thm)],[mp2_2,t1_FOL_11]) ).
cnf(mp3_3,axiom,
( ~ organization(X7,X6)
| reproducibility(X7,sk3(X6,X7),X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_3) ).
cnf(c5,plain,
reproducibility(sk4,sk3(sk6,sk4),sk6),
inference(resolution,[status(thm)],[mp3_3,t1_FOL_10]) ).
cnf(c4,plain,
reproducibility(sk5,sk3(sk7,sk5),sk7),
inference(resolution,[status(thm)],[mp3_3,t1_FOL_11]) ).
cnf(a2_FOL_5,plain,
( ~ organization(X32,X27)
| ~ organization(X28,X26)
| ~ reliability(X32,X25,X27)
| ~ reliability(X28,X29,X26)
| ~ accountability(X32,X30,X27)
| ~ accountability(X28,X34,X26)
| ~ reproducibility(X32,X33,X27)
| ~ reproducibility(X28,X31,X26)
| ~ greater(X31,X33)
| greater(X29,X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2_FOL_5) ).
cnf(c12,plain,
( ~ organization(X158,X163)
| ~ organization(sk5,sk7)
| ~ reliability(X158,X160,X163)
| ~ reliability(sk5,X159,sk7)
| ~ accountability(X158,X162,X163)
| ~ accountability(sk5,X161,sk7)
| ~ reproducibility(X158,X164,X163)
| ~ greater(sk3(sk7,sk5),X164)
| greater(X159,X160) ),
inference(resolution,[status(thm)],[a2_FOL_5,c4]) ).
cnf(t1_FOL_18,negated_conjecture,
greater(sk9,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_18) ).
cnf(t1_FOL_12,negated_conjecture,
reorganization_free(sk4,sk6,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_12) ).
cnf(t1_FOL_13,negated_conjecture,
reorganization_free(sk5,sk7,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_13) ).
cnf(t1_FOL_14,negated_conjecture,
inertia(sk4,sk8,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_14) ).
cnf(t1_FOL_15,negated_conjecture,
inertia(sk5,sk9,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_15) ).
cnf(a3_FOL_9,plain,
( ~ organization(X95,X91)
| ~ organization(X92,X90)
| ~ reorganization_free(X95,X91,X91)
| ~ reorganization_free(X92,X90,X90)
| ~ reproducibility(X95,X89,X91)
| ~ reproducibility(X92,X93,X90)
| ~ inertia(X95,X94,X91)
| ~ inertia(X92,X96,X90)
| ~ greater(X96,X94)
| greater(X93,X89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3_FOL_9) ).
cnf(c37,plain,
( ~ organization(X203,X205)
| ~ organization(sk5,sk7)
| ~ reorganization_free(X203,X205,X205)
| ~ reorganization_free(sk5,sk7,sk7)
| ~ reproducibility(X203,X201,X205)
| ~ reproducibility(sk5,X202,sk7)
| ~ inertia(X203,X204,X205)
| ~ greater(sk9,X204)
| greater(X202,X201) ),
inference(resolution,[status(thm)],[a3_FOL_9,t1_FOL_15]) ).
cnf(c74,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reorganization_free(sk4,sk6,sk6)
| ~ reorganization_free(sk5,sk7,sk7)
| ~ reproducibility(sk4,X253,sk6)
| ~ reproducibility(sk5,X254,sk7)
| ~ greater(sk9,sk8)
| greater(X254,X253) ),
inference(resolution,[status(thm)],[c37,t1_FOL_14]) ).
cnf(c83,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reorganization_free(sk4,sk6,sk6)
| ~ reorganization_free(sk5,sk7,sk7)
| ~ reproducibility(sk4,X262,sk6)
| ~ greater(sk9,sk8)
| greater(sk3(sk7,sk5),X262) ),
inference(resolution,[status(thm)],[c74,c4]) ).
cnf(c86,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reorganization_free(sk4,sk6,sk6)
| ~ reorganization_free(sk5,sk7,sk7)
| ~ greater(sk9,sk8)
| greater(sk3(sk7,sk5),sk3(sk6,sk4)) ),
inference(resolution,[status(thm)],[c83,c5]) ).
cnf(c87,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reorganization_free(sk4,sk6,sk6)
| ~ greater(sk9,sk8)
| greater(sk3(sk7,sk5),sk3(sk6,sk4)) ),
inference(resolution,[status(thm)],[c86,t1_FOL_13]) ).
cnf(c88,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ greater(sk9,sk8)
| greater(sk3(sk7,sk5),sk3(sk6,sk4)) ),
inference(resolution,[status(thm)],[c87,t1_FOL_12]) ).
cnf(c89,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| greater(sk3(sk7,sk5),sk3(sk6,sk4)) ),
inference(resolution,[status(thm)],[c88,t1_FOL_18]) ).
cnf(c90,plain,
( ~ organization(sk4,sk6)
| greater(sk3(sk7,sk5),sk3(sk6,sk4)) ),
inference(resolution,[status(thm)],[c89,t1_FOL_11]) ).
cnf(c92,plain,
greater(sk3(sk7,sk5),sk3(sk6,sk4)),
inference(resolution,[status(thm)],[c90,t1_FOL_10]) ).
cnf(c94,plain,
( ~ organization(X268,X269)
| ~ organization(sk5,sk7)
| ~ reliability(X268,X270,X269)
| ~ reliability(sk5,X271,sk7)
| ~ accountability(X268,X267,X269)
| ~ accountability(sk5,X272,sk7)
| ~ reproducibility(X268,sk3(sk6,sk4),X269)
| greater(X271,X270) ),
inference(resolution,[status(thm)],[c92,c12]) ).
cnf(c96,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X276,sk6)
| ~ reliability(sk5,X273,sk7)
| ~ accountability(sk4,X275,sk6)
| ~ accountability(sk5,X274,sk7)
| greater(X273,X276) ),
inference(resolution,[status(thm)],[c94,c5]) ).
cnf(c97,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X283,sk6)
| ~ reliability(sk5,X282,sk7)
| ~ accountability(sk4,X281,sk6)
| greater(X282,X283) ),
inference(resolution,[status(thm)],[c96,c2]) ).
cnf(c99,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X284,sk6)
| ~ reliability(sk5,X285,sk7)
| greater(X285,X284) ),
inference(resolution,[status(thm)],[c97,c3]) ).
cnf(c100,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X286,sk6)
| greater(sk1(sk7,sk5),X286) ),
inference(resolution,[status(thm)],[c99,c0]) ).
cnf(c101,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| greater(sk1(sk7,sk5),sk1(sk6,sk4)) ),
inference(resolution,[status(thm)],[c100,c1]) ).
cnf(c102,plain,
( ~ organization(sk4,sk6)
| greater(sk1(sk7,sk5),sk1(sk6,sk4)) ),
inference(resolution,[status(thm)],[c101,t1_FOL_11]) ).
cnf(c103,plain,
greater(sk1(sk7,sk5),sk1(sk6,sk4)),
inference(resolution,[status(thm)],[c102,t1_FOL_10]) ).
cnf(a2_FOL_6,plain,
( ~ organization(X49,X44)
| ~ organization(X45,X43)
| ~ reliability(X49,X42,X44)
| ~ reliability(X45,X46,X43)
| ~ accountability(X49,X47,X44)
| ~ accountability(X45,X51,X43)
| ~ reproducibility(X49,X50,X44)
| ~ reproducibility(X45,X48,X43)
| ~ greater(X48,X50)
| greater(X51,X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2_FOL_6) ).
cnf(c17,plain,
( ~ organization(X221,X217)
| ~ organization(sk5,sk7)
| ~ reliability(X221,X218,X217)
| ~ reliability(sk5,X220,sk7)
| ~ accountability(X221,X222,X217)
| ~ accountability(sk5,X219,sk7)
| ~ reproducibility(X221,X216,X217)
| ~ greater(sk3(sk7,sk5),X216)
| greater(X219,X222) ),
inference(resolution,[status(thm)],[a2_FOL_6,c4]) ).
cnf(c95,plain,
( ~ organization(X295,X291)
| ~ organization(sk5,sk7)
| ~ reliability(X295,X292,X291)
| ~ reliability(sk5,X294,sk7)
| ~ accountability(X295,X293,X291)
| ~ accountability(sk5,X296,sk7)
| ~ reproducibility(X295,sk3(sk6,sk4),X291)
| greater(X296,X293) ),
inference(resolution,[status(thm)],[c92,c17]) ).
cnf(c106,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X298,sk6)
| ~ reliability(sk5,X297,sk7)
| ~ accountability(sk4,X299,sk6)
| ~ accountability(sk5,X300,sk7)
| greater(X300,X299) ),
inference(resolution,[status(thm)],[c95,c5]) ).
cnf(c107,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X303,sk6)
| ~ reliability(sk5,X301,sk7)
| ~ accountability(sk4,X302,sk6)
| greater(sk2(sk7,sk5),X302) ),
inference(resolution,[status(thm)],[c106,c2]) ).
cnf(c108,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X305,sk6)
| ~ reliability(sk5,X304,sk7)
| greater(sk2(sk7,sk5),sk2(sk6,sk4)) ),
inference(resolution,[status(thm)],[c107,c3]) ).
cnf(c109,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X310,sk6)
| greater(sk2(sk7,sk5),sk2(sk6,sk4)) ),
inference(resolution,[status(thm)],[c108,c0]) ).
cnf(c112,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| greater(sk2(sk7,sk5),sk2(sk6,sk4)) ),
inference(resolution,[status(thm)],[c109,c1]) ).
cnf(c113,plain,
( ~ organization(sk4,sk6)
| greater(sk2(sk7,sk5),sk2(sk6,sk4)) ),
inference(resolution,[status(thm)],[c112,t1_FOL_11]) ).
cnf(c114,plain,
greater(sk2(sk7,sk5),sk2(sk6,sk4)),
inference(resolution,[status(thm)],[c113,t1_FOL_10]) ).
cnf(t1_FOL_16,negated_conjecture,
survival_chance(sk4,sk10,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_16) ).
cnf(t1_FOL_17,negated_conjecture,
survival_chance(sk5,sk11,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_17) ).
cnf(a1_FOL_4,plain,
( ~ organization(X15,X10)
| ~ organization(X11,X9)
| ~ reliability(X15,X8,X10)
| ~ reliability(X11,X12,X9)
| ~ accountability(X15,X13,X10)
| ~ accountability(X11,X17,X9)
| ~ survival_chance(X15,X16,X10)
| ~ survival_chance(X11,X14,X9)
| ~ greater(X12,X8)
| ~ greater(X17,X13)
| greater(X14,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1_FOL_4) ).
cnf(c8,plain,
( ~ organization(X121,X122)
| ~ organization(sk5,sk7)
| ~ reliability(X121,X120,X122)
| ~ reliability(sk5,X119,sk7)
| ~ accountability(X121,X123,X122)
| ~ accountability(sk5,X118,sk7)
| ~ survival_chance(X121,X117,X122)
| ~ greater(X119,X120)
| ~ greater(X118,X123)
| greater(sk11,X117) ),
inference(resolution,[status(thm)],[a1_FOL_4,t1_FOL_17]) ).
cnf(c50,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X277,sk6)
| ~ reliability(sk5,X279,sk7)
| ~ accountability(sk4,X278,sk6)
| ~ accountability(sk5,X280,sk7)
| ~ greater(X279,X277)
| ~ greater(X280,X278)
| greater(sk11,sk10) ),
inference(resolution,[status(thm)],[c8,t1_FOL_16]) ).
cnf(c98,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X328,sk6)
| ~ reliability(sk5,X327,sk7)
| ~ accountability(sk4,X326,sk6)
| ~ greater(X327,X328)
| ~ greater(sk2(sk7,sk5),X326)
| greater(sk11,sk10) ),
inference(resolution,[status(thm)],[c50,c2]) ).
cnf(c120,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X330,sk6)
| ~ reliability(sk5,X329,sk7)
| ~ accountability(sk4,sk2(sk6,sk4),sk6)
| ~ greater(X329,X330)
| greater(sk11,sk10) ),
inference(resolution,[status(thm)],[c98,c114]) ).
cnf(c121,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X335,sk6)
| ~ reliability(sk5,X336,sk7)
| ~ greater(X336,X335)
| greater(sk11,sk10) ),
inference(resolution,[status(thm)],[c120,c3]) ).
cnf(c122,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,X337,sk6)
| ~ greater(sk1(sk7,sk5),X337)
| greater(sk11,sk10) ),
inference(resolution,[status(thm)],[c121,c0]) ).
cnf(c123,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| ~ reliability(sk4,sk1(sk6,sk4),sk6)
| greater(sk11,sk10) ),
inference(resolution,[status(thm)],[c122,c103]) ).
cnf(c124,plain,
( ~ organization(sk4,sk6)
| ~ organization(sk5,sk7)
| greater(sk11,sk10) ),
inference(resolution,[status(thm)],[c123,c1]) ).
cnf(c125,plain,
( ~ organization(sk4,sk6)
| greater(sk11,sk10) ),
inference(resolution,[status(thm)],[c124,t1_FOL_11]) ).
cnf(c126,plain,
greater(sk11,sk10),
inference(resolution,[status(thm)],[c125,t1_FOL_10]) ).
cnf(c128,plain,
$false,
inference(resolution,[status(thm)],[c126,t1_FOL_19]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT001-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n027.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 11:36:30 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.02/0.39 (re.compile("\."), Token.FullStop),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.02/0.39 (re.compile("\("), Token.OpenPar),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.02/0.39 (re.compile("\)"), Token.ClosePar),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.02/0.39 (re.compile("\["), Token.OpenSquare),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.02/0.39 (re.compile("\]"), Token.CloseSquare),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.02/0.39 (re.compile("~\|"), Token.Nor),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.02/0.39 (re.compile("\|"), Token.Or),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.02/0.39 (re.compile("\?"), Token.Existential),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.02/0.39 (re.compile("\s+"), Token.WhiteSpace),
% 0.02/0.39 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.02/0.39 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.02/0.42 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.02/0.42 """
% 0.02/0.42 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.02/0.42 """
% 0.02/0.46 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.02/0.46 """
% 0.24/0.59 % Version: 1.5
% 0.24/0.59 % SZS status Unsatisfiable
% 0.24/0.59 % SZS output start CNFRefutation
% See solution above
% 0.24/0.59
% 0.24/0.59 % Initial clauses : 19
% 0.24/0.59 % Processed clauses : 126
% 0.24/0.59 % Factors computed : 22
% 0.24/0.59 % Resolvents computed: 107
% 0.24/0.59 % Tautologies deleted: 0
% 0.24/0.59 % Forward subsumed : 13
% 0.24/0.59 % Backward subsumed : 25
% 0.24/0.59 % -------- CPU Time ---------
% 0.24/0.59 % User time : 0.206 s
% 0.24/0.59 % System time : 0.022 s
% 0.24/0.59 % Total time : 0.228 s
%------------------------------------------------------------------------------