%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT024+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 : Sun Sep 27 08:01:04 AM UTC 2026
% Result : Theorem 10.99s 3.21s
% Output : CNFRefutation 10.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT024+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n018.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 00:06:36 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.99/3.21 % SZS status Theorem for theBenchmark.p
% 10.99/3.21 % SZS output start CNFRefutation for theBenchmark.p
% 10.99/3.21 fof(mp_time_point_occur, axiom, ! [X0] : ! [X1] : (((environment(X0) & subpopulations('first$umovers','efficient$uproducers',X0,X1)) => 'in$uenvironment'(X0,X1)))).
% 10.99/3.21 fof(mp_positive_number_of_organizations, axiom, ! [X0] : ! [X1] : (((environment(X0) & subpopulations('first$umovers','efficient$uproducers',X0,X1)) => greater('number$uof$uorganizations'(X0,X1),zero)))).
% 10.99/3.21 fof(mp_equilibrium, axiom, ! [X0] : ! [X1] : (((environment(X0) & 'greater$uor$uequal'(X1,equilibrium(X0))) => ~greater(equilibrium(X0),X1)))).
% 10.99/3.21 fof(a3, hypothesis, ! [X0] : ! [X1] : (((environment(X0) & ('in$uenvironment'(X0,X1) & greater('number$uof$uorganizations'(X0,X1),zero))) => ((greater(equilibrium(X0),X1) => decreases(resources(X0,X1))) & (~greater(equilibrium(X0),X1) => constant(resources(X0,X1))))))).
% 10.99/3.21 fof(a6, hypothesis, ! [X0] : ! [X1] : (((environment(X0) & 'in$uenvironment'(X0,X1)) => ((decreases(resources(X0,X1)) => ~decreases('number$uof$uorganizations'(X0,X1))) & (constant(resources(X0,X1)) => constant('number$uof$uorganizations'(X0,X1))))))).
% 10.99/3.21 fof(l7, hypothesis, ! [X0] : ! [X1] : (((environment(X0) & (subpopulations('first$umovers','efficient$uproducers',X0,X1) & constant('number$uof$uorganizations'(X0,X1)))) => (('growth$urate'('first$umovers',X1) = zero & 'growth$urate'('efficient$uproducers',X1) = zero) | ((greater('growth$urate'('first$umovers',X1),zero) & greater(zero,'growth$urate'('efficient$uproducers',X1))) | (greater('growth$urate'('efficient$uproducers',X1),zero) & greater(zero,'growth$urate'('first$umovers',X1)))))))).
% 10.99/3.21 fof(prove_l6, conjecture, ! [X0] : ! [X1] : (((environment(X0) & (subpopulations('first$umovers','efficient$uproducers',X0,X1) & 'greater$uor$uequal'(X1,equilibrium(X0)))) => (('growth$urate'('first$umovers',X1) = zero & 'growth$urate'('efficient$uproducers',X1) = zero) | ((greater('growth$urate'('first$umovers',X1),zero) & greater(zero,'growth$urate'('efficient$uproducers',X1))) | (greater('growth$urate'('efficient$uproducers',X1),zero) & greater(zero,'growth$urate'('first$umovers',X1)))))))).
% 10.99/3.21 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : (((environment(X0) & (subpopulations('first$umovers','efficient$uproducers',X0,X1) & 'greater$uor$uequal'(X1,equilibrium(X0)))) => (('growth$urate'('first$umovers',X1) = zero & 'growth$urate'('efficient$uproducers',X1) = zero) | ((greater('growth$urate'('first$umovers',X1),zero) & greater(zero,'growth$urate'('efficient$uproducers',X1))) | (greater('growth$urate'('efficient$uproducers',X1),zero) & greater(zero,'growth$urate'('first$umovers',X1))))))), inference(negate_conjecture, [status(cth)], [prove_l6])).
% 10.99/3.21 cnf(c0, plain, ~environment(X0) | ~subpopulations('first$umovers','efficient$uproducers',X0,X1) | 'in$uenvironment'(X0,X1), inference(clausification, [status(esa)], [mp_time_point_occur])).
% 10.99/3.21 cnf(c1, plain, ~environment(X0) | ~subpopulations('first$umovers','efficient$uproducers',X0,X1) | greater('number$uof$uorganizations'(X0,X1),zero), inference(clausification, [status(esa)], [mp_positive_number_of_organizations])).
% 10.99/3.21 cnf(c2, plain, ~environment(X0) | ~'greater$uor$uequal'(X1,equilibrium(X0)) | ~greater(equilibrium(X0),X1), inference(clausification, [status(esa)], [mp_equilibrium])).
% 10.99/3.21 cnf(c4, plain, constant(resources(X0,X1)) | ~'in$uenvironment'(X0,X1) | ~environment(X0) | ~greater('number$uof$uorganizations'(X0,X1),zero) | greater(equilibrium(X0),X1), inference(clausification, [status(esa)], [a3])).
% 10.99/3.21 cnf(c6, plain, ~environment(X0) | ~'in$uenvironment'(X0,X1) | ~constant(resources(X0,X1)) | constant('number$uof$uorganizations'(X0,X1)), inference(clausification, [status(esa)], [a6])).
% 10.99/3.21 cnf(c7, plain, ~environment(X0) | ~constant('number$uof$uorganizations'(X0,X1)) | ~subpopulations('first$umovers','efficient$uproducers',X0,X1) | 'growth$urate'('first$umovers',X1) = zero | X2(X1), inference(clausification, [status(esa)], [l7])).
% 10.99/3.21 cnf(c8, plain, X0(X1) | ~environment(X2) | 'growth$urate'('efficient$uproducers',X1) = zero | ~constant('number$uof$uorganizations'(X2,X1)) | ~subpopulations('first$umovers','efficient$uproducers',X2,X1), inference(clausification, [status(esa)], [l7])).
% 10.99/3.21 cnf(c9, plain, ~X0(X1) | greater('growth$urate'('first$umovers',X1),zero) | greater('growth$urate'('efficient$uproducers',X1),zero), inference(clausification, [status(esa)], [l7])).
% 10.99/3.21 cnf(c10, plain, ~X0(X1) | greater('growth$urate'('first$umovers',X1),zero) | greater(zero,'growth$urate'('first$umovers',X1)), inference(clausification, [status(esa)], [l7])).
% 10.99/3.21 cnf(c11, plain, ~X0(X1) | greater(zero,'growth$urate'('efficient$uproducers',X1)) | greater('growth$urate'('efficient$uproducers',X1),zero), inference(clausification, [status(esa)], [l7])).
% 10.99/3.21 cnf(c12, plain, ~X0(X1) | greater(zero,'growth$urate'('efficient$uproducers',X1)) | greater(zero,'growth$urate'('first$umovers',X1)), inference(clausification, [status(esa)], [l7])).
% 10.99/3.21 cnf(c13, plain, environment(sK13), inference(clausification, [status(esa)], [negated_conjecture])).
% 10.99/3.21 cnf(c14, plain, subpopulations('first$umovers','efficient$uproducers',sK13,sK14), inference(clausification, [status(esa)], [negated_conjecture])).
% 10.99/3.21 cnf(c15, plain, 'greater$uor$uequal'(sK14,equilibrium(sK13)), inference(clausification, [status(esa)], [negated_conjecture])).
% 10.99/3.21 cnf(c16, plain, 'growth$urate'('first$umovers',sK14) != zero | 'growth$urate'('efficient$uproducers',sK14) != zero, inference(clausification, [status(esa)], [negated_conjecture])).
% 10.99/3.21 cnf(c17, plain, ~greater('growth$urate'('first$umovers',sK14),zero) | ~greater(zero,'growth$urate'('efficient$uproducers',sK14)), inference(clausification, [status(esa)], [negated_conjecture])).
% 10.99/3.21 cnf(c18, plain, ~greater('growth$urate'('efficient$uproducers',sK14),zero) | ~greater(zero,'growth$urate'('first$umovers',sK14)), inference(clausification, [status(esa)], [negated_conjecture])).
% 10.99/3.21 cnf(d0, plain, 'growth$urate'('first$umovers',sK14) = zero | ~environment(sK13) | ~constant('number$uof$uorganizations'(sK13,sK14)) | 'Ts10'(sK14), inference(resolution, [status(thm)], [c7,c14])).
% 10.99/3.21 cnf(d1, plain, 'growth$urate'('first$umovers',sK14) = zero | ~constant('number$uof$uorganizations'(sK13,sK14)) | 'Ts10'(sK14), inference(resolution, [status(thm)], [c13,d0])).
% 10.99/3.21 cnf(d2, plain, ~environment(sK13) | greater('number$uof$uorganizations'(sK13,sK14),zero), inference(resolution, [status(thm)], [c14,c1])).
% 10.99/3.21 cnf(d3, plain, greater('number$uof$uorganizations'(sK13,sK14),zero), inference(resolution, [status(thm)], [c13,d2])).
% 10.99/3.21 cnf(d4, plain, ~environment(sK13) | ~'in$uenvironment'(sK13,sK14) | greater(equilibrium(sK13),sK14) | constant(resources(sK13,sK14)), inference(resolution, [status(thm)], [d3,c4])).
% 10.99/3.21 cnf(d5, plain, ~'in$uenvironment'(sK13,sK14) | greater(equilibrium(sK13),sK14) | constant(resources(sK13,sK14)), inference(resolution, [status(thm)], [c13,d4])).
% 10.99/3.21 cnf(d6, plain, ~environment(sK13) | 'in$uenvironment'(sK13,sK14), inference(resolution, [status(thm)], [c14,c0])).
% 10.99/3.21 cnf(d7, plain, 'in$uenvironment'(sK13,sK14), inference(resolution, [status(thm)], [c13,d6])).
% 10.99/3.21 cnf(d8, plain, greater(equilibrium(sK13),sK14) | constant(resources(sK13,sK14)), inference(resolution, [status(thm)], [d7,d5])).
% 10.99/3.21 cnf(d9, plain, ~environment(sK13) | ~greater(equilibrium(sK13),sK14), inference(resolution, [status(thm)], [c2,c15])).
% 10.99/3.21 cnf(d10, plain, ~greater(equilibrium(sK13),sK14), inference(resolution, [status(thm)], [c13,d9])).
% 10.99/3.21 cnf(d11, plain, constant(resources(sK13,sK14)), inference(resolution, [status(thm)], [d10,d8])).
% 10.99/3.21 cnf(d12, plain, ~environment(sK13) | ~'in$uenvironment'(sK13,sK14) | constant('number$uof$uorganizations'(sK13,sK14)), inference(resolution, [status(thm)], [d11,c6])).
% 10.99/3.21 cnf(d13, plain, ~'in$uenvironment'(sK13,sK14) | constant('number$uof$uorganizations'(sK13,sK14)), inference(resolution, [status(thm)], [c13,d12])).
% 10.99/3.21 cnf(d14, plain, constant('number$uof$uorganizations'(sK13,sK14)), inference(resolution, [status(thm)], [d7,d13])).
% 10.99/3.21 cnf(d15, plain, 'growth$urate'('first$umovers',sK14) = zero | 'Ts10'(sK14), inference(resolution, [status(thm)], [d14,d1])).
% 10.99/3.21 cnf(d16, plain, greater('growth$urate'('first$umovers',sK14),zero) | ~'Ts10'(sK14) | ~greater(zero,'growth$urate'('first$umovers',sK14)), inference(resolution, [status(thm)], [c9,c18])).
% 10.99/3.21 cnf(d17, plain, greater(zero,'growth$urate'('first$umovers',sK14)) | ~'Ts10'(sK14) | ~greater(zero,'growth$urate'('efficient$uproducers',sK14)), inference(resolution, [status(thm)], [c10,c17])).
% 10.99/3.21 cnf(d18, plain, greater(zero,'growth$urate'('first$umovers',sK14)) | ~'Ts10'(sK14) | greater(zero,'growth$urate'('first$umovers',sK14)) | ~'Ts10'(sK14), inference(resolution, [status(thm)], [c12,d17])).
% 10.99/3.21 cnf(d19, plain, ~'Ts10'(sK14) | greater('growth$urate'('first$umovers',sK14),zero) | ~'Ts10'(sK14), inference(resolution, [status(thm)], [d18,d16])).
% 10.99/3.21 cnf(d20, plain, ~'Ts10'(sK14) | ~greater(zero,'growth$urate'('efficient$uproducers',sK14)), inference(resolution, [status(thm)], [d19,c17])).
% 10.99/3.21 cnf(d21, plain, greater(zero,'growth$urate'('efficient$uproducers',sK14)) | ~'Ts10'(sK14) | ~greater(zero,'growth$urate'('first$umovers',sK14)), inference(resolution, [status(thm)], [c11,c18])).
% 10.99/3.21 cnf(d22, plain, greater(zero,'growth$urate'('efficient$uproducers',sK14)) | ~'Ts10'(sK14) | ~'Ts10'(sK14), inference(resolution, [status(thm)], [d21,d18])).
% 10.99/3.21 cnf(d23, plain, ~'Ts10'(sK14) | ~'Ts10'(sK14), inference(resolution, [status(thm)], [d22,d20])).
% 10.99/3.21 cnf(d24, plain, 'growth$urate'('first$umovers',sK14) = zero, inference(resolution, [status(thm)], [d23,d15])).
% 10.99/3.21 cnf(d25, plain, 'growth$urate'('efficient$uproducers',sK14) = zero | ~environment(sK13) | ~constant('number$uof$uorganizations'(sK13,sK14)) | 'Ts10'(sK14), inference(resolution, [status(thm)], [c8,c14])).
% 10.99/3.21 cnf(d26, plain, 'growth$urate'('efficient$uproducers',sK14) = zero | ~constant('number$uof$uorganizations'(sK13,sK14)) | 'Ts10'(sK14), inference(resolution, [status(thm)], [c13,d25])).
% 10.99/3.21 cnf(d27, plain, 'growth$urate'('efficient$uproducers',sK14) = zero | 'Ts10'(sK14), inference(resolution, [status(thm)], [d14,d26])).
% 10.99/3.21 cnf(d28, plain, 'growth$urate'('efficient$uproducers',sK14) = zero, inference(resolution, [status(thm)], [d23,d27])).
% 10.99/3.21 cnf(d29, plain, 'growth$urate'('first$umovers',sK14) != zero, inference(resolution, [status(thm)], [d28,c16])).
% 10.99/3.21 cnf(d30, plain, zero != zero, inference(demodulation, [status(thm)], [d29,d24])).
% 10.99/3.21 cnf(d31, plain, $false, inference(equality_resolution, [status(thm)], [d30])).
% 10.99/3.21 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------