%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT007-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:37 AM UTC 2026
% Result : Unsatisfiable 1.37s 1.65s
% Output : CNFRefutation 1.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 14
% Syntax : Number of clauses : 49 ( 17 unt; 20 nHn; 49 RR)
% Number of literals : 216 ( 0 equ; 132 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 : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 81 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t7_FOL_17,negated_conjecture,
~ greater(sk5,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_17) ).
cnf(t7_FOL_10,negated_conjecture,
organization(sk4,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_10) ).
cnf(t7_FOL_9,negated_conjecture,
organization(sk4,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_9) ).
cnf(mp1_1,axiom,
( ~ organization(X2,X3)
| reliability(X2,sk1(X3,X2),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp1_1) ).
cnf(c1,plain,
reliability(sk4,sk1(sk8,sk4),sk8),
inference(resolution,[status(thm)],[mp1_1,t7_FOL_10]) ).
cnf(t7_FOL_16,negated_conjecture,
~ greater(sk8,sk10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_16) ).
cnf(t7_FOL_14,negated_conjecture,
~ greater(sk9,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_14) ).
cnf(t7_FOL_15,negated_conjecture,
greater(sk8,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_15) ).
cnf(t7_FOL_11,negated_conjecture,
reorganization(sk4,sk9,sk10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_11) ).
cnf(c0,plain,
reliability(sk4,sk1(sk7,sk4),sk7),
inference(resolution,[status(thm)],[mp1_1,t7_FOL_9]) ).
cnf(mp2_2,axiom,
( ~ organization(X4,X5)
| accountability(X4,sk2(X5,X4),X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp2_2) ).
cnf(c2,plain,
accountability(sk4,sk2(sk7,sk4),sk7),
inference(resolution,[status(thm)],[mp2_2,t7_FOL_9]) ).
cnf(c3,plain,
accountability(sk4,sk2(sk8,sk4),sk8),
inference(resolution,[status(thm)],[mp2_2,t7_FOL_10]) ).
cnf(a6_FOL_7,plain,
( ~ organization(X90,X87)
| ~ organization(X90,X88)
| ~ reorganization(X90,X85,X84)
| ~ reliability(X90,X89,X87)
| ~ reliability(X90,X82,X88)
| ~ accountability(X90,X83,X87)
| ~ accountability(X90,X86,X88)
| greater(X85,X87)
| ~ greater(X88,X87)
| greater(X88,X84)
| greater(X89,X82) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a6_FOL_7) ).
cnf(c47,plain,
( ~ organization(sk4,X430)
| ~ organization(sk4,sk8)
| ~ reorganization(sk4,X432,X431)
| ~ reliability(sk4,X429,X430)
| ~ reliability(sk4,X427,sk8)
| ~ accountability(sk4,X428,X430)
| greater(X432,X430)
| ~ greater(sk8,X430)
| greater(sk8,X431)
| greater(X429,X427) ),
inference(resolution,[status(thm)],[a6_FOL_7,c3]) ).
cnf(c155,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| ~ reorganization(sk4,X512,X515)
| ~ reliability(sk4,X513,sk7)
| ~ reliability(sk4,X514,sk8)
| greater(X512,sk7)
| ~ greater(sk8,sk7)
| greater(sk8,X515)
| greater(X513,X514) ),
inference(resolution,[status(thm)],[c47,c2]) ).
cnf(c184,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| ~ reorganization(sk4,X516,X518)
| ~ reliability(sk4,X517,sk7)
| greater(X516,sk7)
| ~ greater(sk8,sk7)
| greater(sk8,X518)
| greater(X517,sk1(sk8,sk4)) ),
inference(resolution,[status(thm)],[c155,c1]) ).
cnf(c185,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| ~ reorganization(sk4,X524,X523)
| greater(X524,sk7)
| ~ greater(sk8,sk7)
| greater(sk8,X523)
| greater(sk1(sk7,sk4),sk1(sk8,sk4)) ),
inference(resolution,[status(thm)],[c184,c0]) ).
cnf(c186,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| greater(sk9,sk7)
| ~ greater(sk8,sk7)
| greater(sk8,sk10)
| greater(sk1(sk7,sk4),sk1(sk8,sk4)) ),
inference(resolution,[status(thm)],[c185,t7_FOL_11]) ).
cnf(c187,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| greater(sk9,sk7)
| greater(sk8,sk10)
| greater(sk1(sk7,sk4),sk1(sk8,sk4)) ),
inference(resolution,[status(thm)],[c186,t7_FOL_15]) ).
cnf(c188,plain,
( ~ organization(sk4,sk7)
| greater(sk9,sk7)
| greater(sk8,sk10)
| greater(sk1(sk7,sk4),sk1(sk8,sk4)) ),
inference(resolution,[status(thm)],[c187,t7_FOL_10]) ).
cnf(c189,plain,
( greater(sk9,sk7)
| greater(sk8,sk10)
| greater(sk1(sk7,sk4),sk1(sk8,sk4)) ),
inference(resolution,[status(thm)],[c188,t7_FOL_9]) ).
cnf(c190,plain,
( greater(sk8,sk10)
| greater(sk1(sk7,sk4),sk1(sk8,sk4)) ),
inference(resolution,[status(thm)],[c189,t7_FOL_14]) ).
cnf(c192,plain,
greater(sk1(sk7,sk4),sk1(sk8,sk4)),
inference(resolution,[status(thm)],[c190,t7_FOL_16]) ).
cnf(t7_FOL_13,negated_conjecture,
reproducibility(sk4,sk6,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_13) ).
cnf(t7_FOL_12,negated_conjecture,
reproducibility(sk4,sk5,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_FOL_12) ).
cnf(a2_FOL_6,plain,
( ~ organization(X57,X54)
| ~ organization(X55,X52)
| ~ reliability(X57,X51,X54)
| ~ reliability(X55,X56,X52)
| ~ accountability(X57,X49,X54)
| ~ accountability(X55,X50,X52)
| ~ reproducibility(X57,X53,X54)
| ~ reproducibility(X55,X58,X52)
| ~ greater(X56,X51)
| ~ greater(X50,X49)
| greater(X58,X53) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2_FOL_6) ).
cnf(c31,plain,
( ~ organization(X348,X350)
| ~ organization(sk4,sk7)
| ~ reliability(X348,X347,X350)
| ~ reliability(sk4,X349,sk7)
| ~ accountability(X348,X345,X350)
| ~ accountability(sk4,X344,sk7)
| ~ reproducibility(X348,X346,X350)
| ~ greater(X349,X347)
| ~ greater(X344,X345)
| greater(sk5,X346) ),
inference(resolution,[status(thm)],[a2_FOL_6,t7_FOL_12]) ).
cnf(c127,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| ~ reliability(sk4,X545,sk8)
| ~ reliability(sk4,X548,sk7)
| ~ accountability(sk4,X547,sk8)
| ~ accountability(sk4,X546,sk7)
| ~ greater(X548,X545)
| ~ greater(X546,X547)
| greater(sk5,sk6) ),
inference(resolution,[status(thm)],[c31,t7_FOL_13]) ).
cnf(c195,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| ~ reliability(sk4,X550,sk8)
| ~ reliability(sk4,X549,sk7)
| ~ accountability(sk4,X551,sk8)
| ~ greater(X549,X550)
| ~ greater(sk2(sk7,sk4),X551)
| greater(sk5,sk6) ),
inference(resolution,[status(thm)],[c127,c2]) ).
cnf(a6_FOL_8,plain,
( ~ organization(X104,X101)
| ~ organization(X104,X102)
| ~ reorganization(X104,X99,X98)
| ~ reliability(X104,X103,X101)
| ~ reliability(X104,X96,X102)
| ~ accountability(X104,X97,X101)
| ~ accountability(X104,X100,X102)
| greater(X99,X101)
| ~ greater(X102,X101)
| greater(X102,X98)
| greater(X97,X100) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a6_FOL_8) ).
cnf(c52,plain,
( ~ organization(sk4,X464)
| ~ organization(sk4,sk8)
| ~ reorganization(sk4,X463,X462)
| ~ reliability(sk4,X461,X464)
| ~ reliability(sk4,X466,sk8)
| ~ accountability(sk4,X465,X464)
| greater(X463,X464)
| ~ greater(sk8,X464)
| greater(sk8,X462)
| greater(X465,sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[a6_FOL_8,c3]) ).
cnf(c167,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| ~ reorganization(sk4,X625,X624)
| ~ reliability(sk4,X623,sk7)
| ~ reliability(sk4,X622,sk8)
| greater(X625,sk7)
| ~ greater(sk8,sk7)
| greater(sk8,X624)
| greater(sk2(sk7,sk4),sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[c52,c2]) ).
cnf(c214,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| ~ reorganization(sk4,X627,X628)
| ~ reliability(sk4,X626,sk7)
| greater(X627,sk7)
| ~ greater(sk8,sk7)
| greater(sk8,X628)
| greater(sk2(sk7,sk4),sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[c167,c1]) ).
cnf(c215,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| ~ reorganization(sk4,X629,X630)
| greater(X629,sk7)
| ~ greater(sk8,sk7)
| greater(sk8,X630)
| greater(sk2(sk7,sk4),sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[c214,c0]) ).
cnf(c216,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| greater(sk9,sk7)
| ~ greater(sk8,sk7)
| greater(sk8,sk10)
| greater(sk2(sk7,sk4),sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[c215,t7_FOL_11]) ).
cnf(c217,plain,
( ~ organization(sk4,sk7)
| ~ organization(sk4,sk8)
| greater(sk9,sk7)
| greater(sk8,sk10)
| greater(sk2(sk7,sk4),sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[c216,t7_FOL_15]) ).
cnf(c218,plain,
( ~ organization(sk4,sk7)
| greater(sk9,sk7)
| greater(sk8,sk10)
| greater(sk2(sk7,sk4),sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[c217,t7_FOL_10]) ).
cnf(c219,plain,
( greater(sk9,sk7)
| greater(sk8,sk10)
| greater(sk2(sk7,sk4),sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[c218,t7_FOL_9]) ).
cnf(c221,plain,
( greater(sk8,sk10)
| greater(sk2(sk7,sk4),sk2(sk8,sk4)) ),
inference(resolution,[status(thm)],[c219,t7_FOL_14]) ).
cnf(c231,plain,
greater(sk2(sk7,sk4),sk2(sk8,sk4)),
inference(resolution,[status(thm)],[c221,t7_FOL_16]) ).
cnf(c246,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| ~ reliability(sk4,X643,sk8)
| ~ reliability(sk4,X642,sk7)
| ~ accountability(sk4,sk2(sk8,sk4),sk8)
| ~ greater(X642,X643)
| greater(sk5,sk6) ),
inference(resolution,[status(thm)],[c231,c195]) ).
cnf(c248,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| ~ reliability(sk4,X644,sk8)
| ~ reliability(sk4,X645,sk7)
| ~ greater(X645,X644)
| greater(sk5,sk6) ),
inference(resolution,[status(thm)],[c246,c3]) ).
cnf(c249,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| ~ reliability(sk4,X649,sk8)
| ~ greater(sk1(sk7,sk4),X649)
| greater(sk5,sk6) ),
inference(resolution,[status(thm)],[c248,c0]) ).
cnf(c251,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| ~ reliability(sk4,sk1(sk8,sk4),sk8)
| greater(sk5,sk6) ),
inference(resolution,[status(thm)],[c249,c192]) ).
cnf(c252,plain,
( ~ organization(sk4,sk8)
| ~ organization(sk4,sk7)
| greater(sk5,sk6) ),
inference(resolution,[status(thm)],[c251,c1]) ).
cnf(c253,plain,
( ~ organization(sk4,sk8)
| greater(sk5,sk6) ),
inference(resolution,[status(thm)],[c252,t7_FOL_9]) ).
cnf(c254,plain,
greater(sk5,sk6),
inference(resolution,[status(thm)],[c253,t7_FOL_10]) ).
cnf(c255,plain,
$false,
inference(resolution,[status(thm)],[c254,t7_FOL_17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT007-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.34 % Computer : n006.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 7 11:44:01 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.40 (re.compile("\."), Token.FullStop),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.40 (re.compile("\("), Token.OpenPar),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.40 (re.compile("\)"), Token.ClosePar),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.40 (re.compile("\["), Token.OpenSquare),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.40 (re.compile("~\|"), Token.Nor),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.40 (re.compile("\|"), Token.Or),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.40 (re.compile("\?"), Token.Existential),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.47 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.47 """
% 0.23/0.47 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.47 """
% 0.32/0.56 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.56 """
% 1.37/1.65 % Version: 1.5
% 1.37/1.65 % SZS status Unsatisfiable
% 1.37/1.65 % SZS output start CNFRefutation
% See solution above
% 1.37/1.65
% 1.37/1.65 % Initial clauses : 17
% 1.37/1.65 % Processed clauses : 215
% 1.37/1.65 % Factors computed : 57
% 1.37/1.65 % Resolvents computed: 199
% 1.37/1.65 % Tautologies deleted: 0
% 1.37/1.65 % Forward subsumed : 37
% 1.37/1.65 % Backward subsumed : 41
% 1.37/1.65 % -------- CPU Time ---------
% 1.37/1.65 % User time : 1.281 s
% 1.37/1.65 % System time : 0.031 s
% 1.37/1.65 % Total time : 1.312 s
%------------------------------------------------------------------------------