%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT021+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:40 AM UTC 2026
% Result : Theorem 0.39s 0.63s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 6
% Syntax : Number of formulae : 56 ( 10 unt; 0 def)
% Number of atoms : 184 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 224 ( 96 ~; 82 |; 27 &)
% ( 0 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 60 ( 0 sgn 42 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mp_increase_not_decrease,axiom,
! [X] :
( increases(X)
=> ~ decreases(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_increase_not_decrease) ).
fof(c36,plain,
! [X] :
( increases(X)
=> ~ decreases(X) ),
inference(fof_simplification,[status(thm)],[mp_increase_not_decrease]) ).
fof(c37,plain,
! [X] :
( ~ increases(X)
| ~ decreases(X) ),
inference(fof_nnf,[status(thm)],[c36]) ).
fof(c38,plain,
! [X10] :
( ~ increases(X10)
| ~ decreases(X10) ),
inference(variable_rename,[status(thm)],[c37]) ).
cnf(c39,plain,
( ~ increases(X16)
| ~ decreases(X16) ),
inference(split_conjunct,[status(thm)],[c38]) ).
fof(prove_l3,conjecture,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l3) ).
fof(c13,negated_conjecture,
~ ! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ),
inference(assume_negation,[status(cth)],[prove_l3]) ).
fof(c14,negated_conjecture,
~ ! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ),
inference(fof_simplification,[status(thm)],[c13]) ).
fof(c15,negated_conjecture,
? [E,T] :
( environment(E)
& subpopulations(first_movers,efficient_producers,E,T)
& decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ),
inference(fof_nnf,[status(thm)],[c14]) ).
fof(c16,negated_conjecture,
? [X2,X3] :
( environment(X2)
& subpopulations(first_movers,efficient_producers,X2,X3)
& decreases(difference(disbanding_rate(first_movers,X3),disbanding_rate(efficient_producers,X3))) ),
inference(variable_rename,[status(thm)],[c15]) ).
fof(c17,negated_conjecture,
( environment(skolem0001)
& subpopulations(first_movers,efficient_producers,skolem0001,skolem0002)
& decreases(difference(disbanding_rate(first_movers,skolem0002),disbanding_rate(efficient_producers,skolem0002))) ),
inference(skolemize,[status(esa)],[c16]) ).
cnf(c20,negated_conjecture,
decreases(difference(disbanding_rate(first_movers,skolem0002),disbanding_rate(efficient_producers,skolem0002))),
inference(split_conjunct,[status(thm)],[c17]) ).
cnf(c76,plain,
~ increases(difference(disbanding_rate(first_movers,skolem0002),disbanding_rate(efficient_producers,skolem0002))),
inference(resolution,[status(thm)],[c20,c39]) ).
cnf(c18,negated_conjecture,
environment(skolem0001),
inference(split_conjunct,[status(thm)],[c17]) ).
cnf(c19,negated_conjecture,
subpopulations(first_movers,efficient_producers,skolem0001,skolem0002),
inference(split_conjunct,[status(thm)],[c17]) ).
fof(l4,plain,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> ( ( decreases(resources(E,T))
=> increases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) )
& ( constant(resources(E,T))
=> ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l4) ).
fof(c21,plain,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> ( ( decreases(resources(E,T))
=> increases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) )
& ( constant(resources(E,T))
=> ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ) ) ),
inference(fof_simplification,[status(thm)],[l4]) ).
fof(c22,plain,
! [E,T] :
( ~ environment(E)
| ~ subpopulations(first_movers,efficient_producers,E,T)
| ( ( ~ decreases(resources(E,T))
| increases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) )
& ( ~ constant(resources(E,T))
| ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ) ) ),
inference(fof_nnf,[status(thm)],[c21]) ).
fof(c23,plain,
! [X4,X5] :
( ~ environment(X4)
| ~ subpopulations(first_movers,efficient_producers,X4,X5)
| ( ( ~ decreases(resources(X4,X5))
| increases(difference(disbanding_rate(first_movers,X5),disbanding_rate(efficient_producers,X5))) )
& ( ~ constant(resources(X4,X5))
| ~ decreases(difference(disbanding_rate(first_movers,X5),disbanding_rate(efficient_producers,X5))) ) ) ),
inference(variable_rename,[status(thm)],[c22]) ).
fof(c24,plain,
! [X4,X5] :
( ( ~ environment(X4)
| ~ subpopulations(first_movers,efficient_producers,X4,X5)
| ~ decreases(resources(X4,X5))
| increases(difference(disbanding_rate(first_movers,X5),disbanding_rate(efficient_producers,X5))) )
& ( ~ environment(X4)
| ~ subpopulations(first_movers,efficient_producers,X4,X5)
| ~ constant(resources(X4,X5))
| ~ decreases(difference(disbanding_rate(first_movers,X5),disbanding_rate(efficient_producers,X5))) ) ),
inference(distribute,[status(thm)],[c23]) ).
cnf(c25,plain,
( ~ environment(X118)
| ~ subpopulations(first_movers,efficient_producers,X118,X119)
| ~ decreases(resources(X118,X119))
| increases(difference(disbanding_rate(first_movers,X119),disbanding_rate(efficient_producers,X119))) ),
inference(split_conjunct,[status(thm)],[c24]) ).
cnf(c78,plain,
( ~ environment(skolem0001)
| ~ decreases(resources(skolem0001,skolem0002))
| increases(difference(disbanding_rate(first_movers,skolem0002),disbanding_rate(efficient_producers,skolem0002))) ),
inference(resolution,[status(thm)],[c25,c19]) ).
fof(mp_time_point_in_environment,axiom,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> in_environment(E,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_time_point_in_environment) ).
fof(c43,plain,
! [E,T] :
( ~ environment(E)
| ~ subpopulations(first_movers,efficient_producers,E,T)
| in_environment(E,T) ),
inference(fof_nnf,[status(thm)],[mp_time_point_in_environment]) ).
fof(c44,plain,
! [X13,X14] :
( ~ environment(X13)
| ~ subpopulations(first_movers,efficient_producers,X13,X14)
| in_environment(X13,X14) ),
inference(variable_rename,[status(thm)],[c43]) ).
cnf(c45,plain,
( ~ environment(X91)
| ~ subpopulations(first_movers,efficient_producers,X91,X92)
| in_environment(X91,X92) ),
inference(split_conjunct,[status(thm)],[c44]) ).
cnf(c70,plain,
( ~ environment(skolem0001)
| in_environment(skolem0001,skolem0002) ),
inference(resolution,[status(thm)],[c45,c19]) ).
cnf(c71,plain,
in_environment(skolem0001,skolem0002),
inference(resolution,[status(thm)],[c70,c18]) ).
fof(mp_environment_not_empty,axiom,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> greater(number_of_organizations(E,T),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_environment_not_empty) ).
fof(c40,plain,
! [E,T] :
( ~ environment(E)
| ~ subpopulations(first_movers,efficient_producers,E,T)
| greater(number_of_organizations(E,T),zero) ),
inference(fof_nnf,[status(thm)],[mp_environment_not_empty]) ).
fof(c41,plain,
! [X11,X12] :
( ~ environment(X11)
| ~ subpopulations(first_movers,efficient_producers,X11,X12)
| greater(number_of_organizations(X11,X12),zero) ),
inference(variable_rename,[status(thm)],[c40]) ).
cnf(c42,plain,
( ~ environment(X116)
| ~ subpopulations(first_movers,efficient_producers,X116,X117)
| greater(number_of_organizations(X116,X117),zero) ),
inference(split_conjunct,[status(thm)],[c41]) ).
cnf(c77,plain,
( ~ environment(skolem0001)
| greater(number_of_organizations(skolem0001,skolem0002),zero) ),
inference(resolution,[status(thm)],[c42,c19]) ).
cnf(c79,plain,
greater(number_of_organizations(skolem0001,skolem0002),zero),
inference(resolution,[status(thm)],[c77,c18]) ).
fof(a3,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T)
& greater(number_of_organizations(E,T),zero) )
=> ( ( greater(equilibrium(E),T)
=> decreases(resources(E,T)) )
& ( ~ greater(equilibrium(E),T)
=> constant(resources(E,T)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(c27,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T)
& greater(number_of_organizations(E,T),zero) )
=> ( ( greater(equilibrium(E),T)
=> decreases(resources(E,T)) )
& ( ~ greater(equilibrium(E),T)
=> constant(resources(E,T)) ) ) ),
inference(fof_simplification,[status(thm)],[a3]) ).
fof(c28,plain,
! [E,T] :
( ~ environment(E)
| ~ in_environment(E,T)
| ~ greater(number_of_organizations(E,T),zero)
| ( ( ~ greater(equilibrium(E),T)
| decreases(resources(E,T)) )
& ( greater(equilibrium(E),T)
| constant(resources(E,T)) ) ) ),
inference(fof_nnf,[status(thm)],[c27]) ).
fof(c29,plain,
! [X6,X7] :
( ~ environment(X6)
| ~ in_environment(X6,X7)
| ~ greater(number_of_organizations(X6,X7),zero)
| ( ( ~ greater(equilibrium(X6),X7)
| decreases(resources(X6,X7)) )
& ( greater(equilibrium(X6),X7)
| constant(resources(X6,X7)) ) ) ),
inference(variable_rename,[status(thm)],[c28]) ).
fof(c30,plain,
! [X6,X7] :
( ( ~ environment(X6)
| ~ in_environment(X6,X7)
| ~ greater(number_of_organizations(X6,X7),zero)
| ~ greater(equilibrium(X6),X7)
| decreases(resources(X6,X7)) )
& ( ~ environment(X6)
| ~ in_environment(X6,X7)
| ~ greater(number_of_organizations(X6,X7),zero)
| greater(equilibrium(X6),X7)
| constant(resources(X6,X7)) ) ),
inference(distribute,[status(thm)],[c29]) ).
cnf(c31,plain,
( ~ environment(X135)
| ~ in_environment(X135,X136)
| ~ greater(number_of_organizations(X135,X136),zero)
| ~ greater(equilibrium(X135),X136)
| decreases(resources(X135,X136)) ),
inference(split_conjunct,[status(thm)],[c30]) ).
cnf(c88,plain,
( ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| ~ greater(equilibrium(skolem0001),skolem0002)
| decreases(resources(skolem0001,skolem0002)) ),
inference(resolution,[status(thm)],[c31,c79]) ).
cnf(c26,plain,
( ~ environment(X123)
| ~ subpopulations(first_movers,efficient_producers,X123,X124)
| ~ constant(resources(X123,X124))
| ~ decreases(difference(disbanding_rate(first_movers,X124),disbanding_rate(efficient_producers,X124))) ),
inference(split_conjunct,[status(thm)],[c24]) ).
cnf(c83,plain,
( ~ environment(X125)
| ~ subpopulations(first_movers,efficient_producers,X125,skolem0002)
| ~ constant(resources(X125,skolem0002)) ),
inference(resolution,[status(thm)],[c26,c20]) ).
cnf(c84,plain,
( ~ environment(skolem0001)
| ~ constant(resources(skolem0001,skolem0002)) ),
inference(resolution,[status(thm)],[c83,c19]) ).
cnf(c32,plain,
( ~ environment(X138)
| ~ in_environment(X138,X139)
| ~ greater(number_of_organizations(X138,X139),zero)
| greater(equilibrium(X138),X139)
| constant(resources(X138,X139)) ),
inference(split_conjunct,[status(thm)],[c30]) ).
cnf(c90,plain,
( ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(equilibrium(skolem0001),skolem0002)
| constant(resources(skolem0001,skolem0002)) ),
inference(resolution,[status(thm)],[c32,c79]) ).
cnf(c91,plain,
( ~ environment(skolem0001)
| greater(equilibrium(skolem0001),skolem0002)
| constant(resources(skolem0001,skolem0002)) ),
inference(resolution,[status(thm)],[c90,c71]) ).
cnf(c92,plain,
( greater(equilibrium(skolem0001),skolem0002)
| constant(resources(skolem0001,skolem0002)) ),
inference(resolution,[status(thm)],[c91,c18]) ).
cnf(c95,plain,
( greater(equilibrium(skolem0001),skolem0002)
| ~ environment(skolem0001) ),
inference(resolution,[status(thm)],[c92,c84]) ).
cnf(c96,plain,
greater(equilibrium(skolem0001),skolem0002),
inference(resolution,[status(thm)],[c95,c18]) ).
cnf(c97,plain,
( ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| decreases(resources(skolem0001,skolem0002)) ),
inference(resolution,[status(thm)],[c96,c88]) ).
cnf(c102,plain,
( ~ environment(skolem0001)
| decreases(resources(skolem0001,skolem0002)) ),
inference(resolution,[status(thm)],[c97,c71]) ).
cnf(c103,plain,
decreases(resources(skolem0001,skolem0002)),
inference(resolution,[status(thm)],[c102,c18]) ).
cnf(c104,plain,
( ~ environment(skolem0001)
| increases(difference(disbanding_rate(first_movers,skolem0002),disbanding_rate(efficient_producers,skolem0002))) ),
inference(resolution,[status(thm)],[c103,c78]) ).
cnf(c106,plain,
increases(difference(disbanding_rate(first_movers,skolem0002),disbanding_rate(efficient_producers,skolem0002))),
inference(resolution,[status(thm)],[c104,c18]) ).
cnf(c107,plain,
$false,
inference(resolution,[status(thm)],[c106,c76]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT021+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % 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 12:03:53 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.48 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.21/0.48 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.31/0.57 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.57 """
% 0.39/0.63 % Version: 1.5
% 0.39/0.63 % SZS status Theorem
% 0.39/0.63 % SZS output start CNFRefutation
% See solution above
% 0.39/0.63
% 0.39/0.63 % Initial clauses : 27
% 0.39/0.63 % Processed clauses : 66
% 0.39/0.63 % Factors computed : 5
% 0.39/0.63 % Resolvents computed: 57
% 0.39/0.63 % Tautologies deleted: 6
% 0.39/0.63 % Forward subsumed : 16
% 0.39/0.63 % Backward subsumed : 12
% 0.39/0.63 % -------- CPU Time ---------
% 0.39/0.63 % User time : 0.258 s
% 0.39/0.63 % System time : 0.023 s
% 0.39/0.63 % Total time : 0.281 s
%------------------------------------------------------------------------------